Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
Final term is not finished
(¬(q → p) ∨ (¬((q → p) ∨ (q → p)) ∧ ¬((q → p) ∨ (q → p)))) ↔ (((r ∨ (r ∧ T)) ↔ s) ∨ ¬s)
⇒ logic.propositional.truezeroand(¬(q → p) ∨ (¬((q → p) ∨ (q → p)) ∧ ¬((q → p) ∨ (q → p)))) ↔ (((r ∨ r) ↔ s) ∨ ¬s)