Exercise logic.propositional.cnf.unicode

Description
Proposition to CNF (unicode support)

¬((r ↔ r) ∧ T ∧ T ∧ r ∧ ((r ∧ r) ∨ (¬r ∧ ¬r)) ∧ r)
ready: no

Feedback

Path 1

path[0, 2, 0, 2, 1, 0, 2, 1, 0, 2, 1, 0, 2, 1, 0, 0, 3, 3, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0]
steps30
major rules2
active labels
  • cnf
  • simplify
  • orrules

enter cnf, check, navigator.down, navigator.right, check, navigator.down, navigator.right, check, navigator.down, navigator.right, check, navigator.down, navigator.right, check, navigator.down, check, enter eliminateimplequiv, logic.propositional.defequiv, exit eliminateimplequiv, navigator.up, navigator.up, navigator.up, navigator.up, navigator.up, check, navigator.down, check, enter simplify, enter orrules, logic.propositional.falsezeroor