Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
Final term is not finished(¬(¬q ∨ ¬q ∨ p) ∧ (((r ↔ s) ∧ ¬(¬q ∨ ¬q ∨ p)) ∨ (¬s ∧ ¬(¬q ∨ ¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.idempor(¬(¬q ∨ p) ∧ (((r ↔ s) ∧ ¬(¬q ∨ ¬q ∨ p)) ∨ (¬s ∧ ¬(¬q ∨ ¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.idempor(¬(¬q ∨ p) ∧ (((r ↔ s) ∧ ¬(¬q ∨ p)) ∨ (¬s ∧ ¬(¬q ∨ ¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.idempor(¬(¬q ∨ p) ∧ (((r ↔ s) ∧ ¬(¬q ∨ p)) ∨ (¬s ∧ ¬(¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(¬¬q ∧ ¬p ∧ (((r ↔ s) ∧ ¬(¬q ∨ p)) ∨ (¬s ∧ ¬(¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot(q ∧ ¬p ∧ (((r ↔ s) ∧ ¬(¬q ∨ p)) ∨ (¬s ∧ ¬(¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(q ∧ ¬p ∧ (((r ↔ s) ∧ ¬¬q ∧ ¬p) ∨ (¬s ∧ ¬(¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot(q ∧ ¬p ∧ (((r ↔ s) ∧ q ∧ ¬p) ∨ (¬s ∧ ¬(¬q ∨ p))) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(q ∧ ¬p ∧ (((r ↔ s) ∧ q ∧ ¬p) ∨ (¬s ∧ ¬¬q ∧ ¬p)) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot(q ∧ ¬p ∧ (((r ↔ s) ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.defequiv(q ∧ ¬p ∧ ((((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ ((r ↔ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.defequiv(q ∧ ¬p ∧ ((((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ ((r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.absorpor(q ∧ ¬p ∧ ((((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ ((r ∧ s) ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.oroverand(q ∧ ¬p ∧ ((((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ (r ∨ ¬s) ∧ (s ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.complor(q ∧ ¬p ∧ ((((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ (r ∨ ¬s) ∧ T) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.truezeroand(q ∧ ¬p ∧ ((((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ (r ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.andoveror(q ∧ ¬p ∧ ((r ∧ s ∧ q ∧ ¬p) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ (r ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.absorpor(q ∧ ¬p ∧ ((r ∧ s ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ (r ∨ ¬s)) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.andoveror(q ∧ ¬p ∧ ((((r ∧ s ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ r) ∨ (((r ∧ s ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ ¬s))) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.andoveror(q ∧ ¬p ∧ ((r ∧ s ∧ q ∧ ¬p ∧ r) ∨ (¬s ∧ q ∧ ¬p ∧ r) ∨ (((r ∧ s ∧ q ∧ ¬p) ∨ (¬s ∧ q ∧ ¬p)) ∧ ¬s))) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.andoveror(q ∧ ¬p ∧ ((r ∧ s ∧ q ∧ ¬p ∧ r) ∨ (¬s ∧ q ∧ ¬p ∧ r) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ ¬s))) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.genandoveror(q ∧ ((¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ r) ∨ (¬p ∧ ¬s ∧ q ∧ ¬p ∧ r) ∨ (¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬p ∧ ¬s ∧ q ∧ ¬p ∧ ¬s))) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.genandoveror(q ∧ ¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s ∧ q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.idempand(q ∧ ¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s ∧ q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ ¬s) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.absorpor(q ∧ ¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s ∧ q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.absorpor(q ∧ ¬p ∧ r ∧ s ∧ q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ (¬¬(¬q ∨ p) ∧ ¬((r ↔ s) ∨ ¬s))