Exercise logic.propositional.cnf.unicode

Description
Proposition to CNF (unicode support)

Derivation

Final term is not finished

(r ↔ r) → (¬(r ↔ r) ∨ (¬(T ∧ r) ∧ T))

⇒ logic.propositional.truezeroand

(r ↔ r) → (¬(r ↔ r) ∨ ¬(T ∧ r))

⇒ logic.propositional.truezeroand

(r ↔ r) → (¬(r ↔ r) ∨ ¬r)