Exercise logic.propositional.cnf.unicode
Description
Proposition to CNF (unicode support)
Derivation
Final term is not finished¬(((r ∧ r) ∨ (((¬r ∧ (F ∨ ¬r)) ∨ (r ∧ r) ∨ ¬r) ∧ ((¬r ∧ (F ∨ ¬r)) ∨ (r ∧ r) ∨ F ∨ ¬r))) ∧ r)
⇒ logic.propositional.absorpand¬(((r ∧ r) ∨ ((¬r ∨ (r ∧ r) ∨ ¬r) ∧ ((¬r ∧ (F ∨ ¬r)) ∨ (r ∧ r) ∨ F ∨ ¬r))) ∧ r)
⇒ logic.propositional.falsezeroor¬(((r ∧ r) ∨ ((¬r ∨ (r ∧ r) ∨ ¬r) ∧ ((¬r ∧ (F ∨ ¬r)) ∨ (r ∧ r) ∨ ¬r))) ∧ r)
⇒ logic.propositional.absorpand¬(((r ∧ r) ∨ ((¬r ∨ (r ∧ r) ∨ ¬r) ∧ (¬r ∨ (r ∧ r) ∨ ¬r))) ∧ r)
⇒ logic.propositional.idempand¬((r ∨ ((¬r ∨ (r ∧ r) ∨ ¬r) ∧ (¬r ∨ (r ∧ r) ∨ ¬r))) ∧ r)
⇒ logic.propositional.idempand¬((r ∨ ((¬r ∨ r ∨ ¬r) ∧ (¬r ∨ (r ∧ r) ∨ ¬r))) ∧ r)
⇒ logic.propositional.complor¬((r ∨ ((¬r ∨ T) ∧ (¬r ∨ (r ∧ r) ∨ ¬r))) ∧ r)
⇒ logic.propositional.idempand¬((r ∨ ((¬r ∨ T) ∧ (¬r ∨ r ∨ ¬r))) ∧ r)
⇒ logic.propositional.complor¬((r ∨ ((¬r ∨ T) ∧ (¬r ∨ T))) ∧ r)
⇒ logic.propositional.idempand¬((r ∨ ¬r ∨ T) ∧ r)
⇒ logic.propositional.complor¬((T ∨ T) ∧ r)
⇒ logic.propositional.idempor¬(T ∧ r)