Exercise logic.propositional.dnf.unicode

Description
Proposition to DNF (unicode support)

¬(q → p) ↔ ((r ∧ s) ∨ ¬s ∨ (r ↔ s) ∨ ¬s)
ready: no

Feedback

Path 1

path[0, 2, 0, 2, 1, 0, 0, 0, 5, 6, 0, 2, 0, 0, 0, 0, 0, 2, 0, 2, 1, 0, 0, 0, 1, 3]
steps26
major rules2
active labels
  • dnf
  • andrules

enter dnf, check, navigator.down, navigator.right, check, navigator.down, check, enter simplify, navigator.down, navigator.right, enter orrules, logic.propositional.idempor, exit orrules, navigator.up, exit simplify, navigator.up, navigator.up, check, navigator.down, navigator.right, check, navigator.down, check, enter simplify, enter andrules, logic.propositional.absorpand