# Conversion from PL to CNF

I am trying to convert some formulas into CNF even if I understood both concepts and rules of it I cannot always get a solution. For example I have this statement to convert: $$(p\Leftrightarrow p)\Rightarrow (\neg p \wedge r)$$. Applying the rules I get this formula (that I know it is right since the solution for both formulas is the same according to Wolfram) $$(p \wedge \neg q) \vee (q \wedge \neg p) \vee (\neg p \wedge r)$$. From this position I know I should apply some distributive law to "move the OR inside and the AND outside" but I really don't get how. I already know the result that is $$(\neg p \vee \neg q) \wedge (p \vee q \vee r)$$.

There are several options how you could apply distributive law. Here's one. The version I'm using says that $$(A \land B) \lor C \equiv (A \lor C) \land (B \lor C)$$. Let's apply this to your formula $$(p \land \lnot q) \lor (q \land \lnot p) \lor (\lnot p \land r)$$ Here you can set $$A := p$$, $$B := \lnot q$$ and $$C := (q \land \lnot p) \lor (\lnot p \land r)$$. Then distributivity yields $$(p \lor (q \land \lnot p) \lor (\lnot p \land r)) \land (\lnot q \lor (q \land \lnot p) \lor (\lnot p \land r))$$
We need to apply distributivity a few times more. Consider the left side first. $$(p \lor (q \land \lnot p) \lor (\lnot p \land r)) \equiv [(p \lor q) \land (p \lor \lnot p)] \lor (\lnot p \land r) \equiv (p \lor q) \lor (\lnot p \land r) \\ \equiv (p \lor q \lor \lnot p) \land (p \lor q \lor r) \equiv p \vee q \vee r$$
Here I used the law that $$A \wedge \top \equiv A$$ twice, removing the tautologous $$(p \vee \lnot p)$$ and $$(p \vee q \vee \lnot p)$$.
Let's turn to the right-hand side. By similar reductions as in the first step, you get $$(\lnot q \lor (q \land \lnot p) \lor (\lnot p \land r)) \equiv (\lnot q \lor \lnot p \lor \lnot p) \wedge (\lnot q \lor \lnot p \lor r)$$
By the law that $$(A \lor B) \wedge (A \lor B \lor C) \equiv A \lor B$$, this is equivalent to $$\lnot q \lor \lnot p$$
Thus, combining the results we get $$(p \vee q \vee r) \wedge (\lnot q \lor \lnot p)$$, as desired.