Clause Normal Form

Simplify
Formula	Rewrites to
`P` `<~>` `Q`	`(P` `\|` `Q) & (~P` `\| ~Q)`
`P` `<=>` `Q`	`(P` `=>` `Q) & (Q` `=>` `P)`
`P` `=>` `Q`	`~P` `\|` `Q`

Move negations in
Formula Rewrites to
~∀X P ∃X ~P
~∃X P ∀X ~P
~(P & Q) (~P | ~Q)
~(P | Q) (~P & ~Q)
~~P P

Move quantifiers out
Formula Rewrites to
∀X P & Q ∀X (P & Q)
∃X P & Q ∃X (P & Q)
Q & ∀X P ∀X (Q & P)
Q & ∃X P ∃X (Q & P)
∀X P | Q ∀X (P | Q)
∃X P | Q ∃X (P | Q)
Q | ∀X P ∀X (Q | P)
Q | ∃XP ∃X (Q | P)

Skolemize
Formula Rewrites to
Initially Set γ = {}
∀X P P
and set γ = γ ∪ {X}
∃X P P[X/x(γ)]
where x is a new Skolem functor.

Distribute disjunctions
Formula Rewrites to
P | (Q & R) (P | Q) & (P | R)
(Q & R) | P (Q | P) & (R | P)

Convert to CNF
Formula Rewrites to
P₁ & ... & P_n {P₁,...,P_n}

Move negations in
Formula	Rewrites to
`~∀X` `P`	`∃X ~P`
`~∃X` `P`	`∀X ~P`
`~(P` `&` `Q)`	`(~P` `\| ~Q)`
`~(P` `\|` `Q)`	`(~P` `& ~Q)`
`~~P`	`P`

Move quantifiers out
Formula	Rewrites to
`∀X` `P` `&` `Q`	`∀X (P` `&` `Q)`
`∃X` `P` `&` `Q`	`∃X (P` `&` `Q)`
`Q` `& ∀X` `P`	`∀X (Q` `&` `P)`
`Q` `& ∃X` `P`	`∃X (Q` `&` `P)`
`∀X` `P` `\|` `Q`	`∀X (P` `\|` `Q)`
`∃X` `P` `\|` `Q`	`∃X (P` `\|` `Q)`
`Q` `\| ∀X` `P`	`∀X (Q` `\|` `P)`
`Q` `\| ∃XP`	`∃X (Q` `\|` `P)`

Skolemize
Formula	Rewrites to
Initially	Set `γ = {}`
`∀X` `P`	`P` and set `γ = γ ∪ {X}`
`∃X` `P`	`P[X/x(γ)]` where `x` is a new Skolem functor.

Distribute disjunctions
Formula	Rewrites to
`P` `\| (Q` `&` `R)`	`(P` `\|` `Q) & (P` `\|` `R)`
`(Q` `&` `R) \|` `P`	`(Q` `\|` `P) & (R` `\|` `P)`

Convert to CNF
Formula	Rewrites to
`P`₁ `& ... &` `P`_n	`{P`₁`,...,P`_n`}`