Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivation
((¬(¬q ∨ p) ∧ (¬s ∨ (r ↔ s))) ∨ ¬¬(¬q ∨ p)) ∧ ((¬(¬q ∨ p) ∧ (¬s ∨ (r ↔ s))) ∨ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot((¬(¬q ∨ p) ∧ (¬s ∨ (r ↔ s))) ∨ ¬q ∨ p) ∧ ((¬(¬q ∨ p) ∧ (¬s ∨ (r ↔ s))) ∨ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.oroverand(¬(¬q ∨ p) ∨ ¬q ∨ p) ∧ (¬s ∨ (r ↔ s) ∨ ¬q ∨ p) ∧ ((¬(¬q ∨ p) ∧ (¬s ∨ (r ↔ s))) ∨ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.complorT ∧ (¬s ∨ (r ↔ s) ∨ ¬q ∨ p) ∧ ((¬(¬q ∨ p) ∧ (¬s ∨ (r ↔ s))) ∨ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.truezeroand(¬s ∨ (r ↔ s) ∨ ¬q ∨ p) ∧ ((¬(¬q ∨ p) ∧ (¬s ∨ (r ↔ s))) ∨ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(¬s ∨ (r ↔ s) ∨ ¬q ∨ p) ∧ ((¬¬q ∧ ¬p ∧ (¬s ∨ (r ↔ s))) ∨ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.notnot(¬s ∨ (r ↔ s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ↔ s))) ∨ ¬((r ↔ s) ∨ ¬s))
⇒ logic.propositional.demorganor(¬s ∨ (r ↔ s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ↔ s))) ∨ (¬(r ↔ s) ∧ ¬¬s))
⇒ logic.propositional.notnot(¬s ∨ (r ↔ s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ↔ s))) ∨ (¬(r ↔ s) ∧ s))
⇒ logic.propositional.defequiv(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ↔ s))) ∨ (¬(r ↔ s) ∧ s))
⇒ logic.propositional.defequiv(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬(r ↔ s) ∧ s))
⇒ logic.propositional.defequiv(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬((r ∧ s) ∨ (¬r ∧ ¬s)) ∧ s))
⇒ logic.propositional.demorganor(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬(r ∧ s) ∧ ¬(¬r ∧ ¬s) ∧ s))
⇒ logic.propositional.demorganand(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬(r ∧ s) ∧ (¬¬r ∨ ¬¬s) ∧ s))
⇒ logic.propositional.notnot(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬(r ∧ s) ∧ (r ∨ ¬¬s) ∧ s))
⇒ logic.propositional.notnot(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬(r ∧ s) ∧ (r ∨ s) ∧ s))
⇒ logic.propositional.absorpand(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬(r ∧ s) ∧ s))
⇒ logic.propositional.demorganand(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ ((¬r ∨ ¬s) ∧ s))
⇒ logic.propositional.andoveror(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬r ∧ s) ∨ (¬s ∧ s))
⇒ logic.propositional.compland(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬r ∧ s) ∨ F)
⇒ logic.propositional.falsezeroor(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s))) ∨ (¬r ∧ s))
⇒ logic.propositional.genandoveror(¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ((q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ r ∧ s) ∨ (q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬r ∧ s))
⇒ logic.propositional.genandoveror((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.genandoveror(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬q ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.compland(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (F ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.falsezeroand(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ F ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.falsezeroor(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.genandoveror(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬q ∧ q ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.compland(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (F ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.falsezeroand(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ F ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.falsezeroor(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.genandoveror(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬q ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.compland(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (F ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.falsezeroand(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ F ∨ (p ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.falsezeroor(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ ((¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬q ∨ p) ∧ ¬r ∧ s)
⇒ logic.propositional.genandoveror(¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬s) ∨ (¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ r ∧ s) ∨ (p ∧ q ∧ ¬p ∧ r ∧ s) ∨ (¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (r ∧ s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬r ∧ ¬s ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (p ∧ q ∧ ¬p ∧ ¬r ∧ ¬s) ∨ (¬s ∧ ¬r ∧ s) ∨ (r ∧ s ∧ ¬r ∧ s) ∨ (¬r ∧ ¬s ∧ ¬r ∧ s) ∨ (¬q ∧ ¬r ∧ s) ∨ (p ∧ ¬r ∧ s)