DescriptionProposition to CNF (unicode support)
¬((q → r) → ¬q)
(¬q ∧ ¬(p → q)) → p
((q ∨ p) → (q → p)) → (r ∧ q ∧ p)
p ↔ (p ∧ q)
(p ∧ q) ∨ (p ↔ r)