Clause Normal Form Tables

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`}`