Exercise

Exercise logic.propositional.cnf.unicode

Description
Proposition to CNF (unicode support)

¬((r ↔ r) ∧ r)

ready: no

Feedback

(no onefirst)
allfirsts (0)
allapplications
derivation
microsteps

Path 1

path [0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 1]
steps 22
major rules 3
active labels
cnf
andrules

enter cnf, check, navigator.down, check, enter simplify, enter orrules, logic.propositional.falsezeroor, exit orrules, exit simplify, navigator.up, check, navigator.down, navigator.right, check, enter simplify, enter orrules, logic.propositional.falsezeroor, exit orrules, exit simplify, navigator.up, enter andrules, logic.propositional.truezeroand

path	[0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 1]
steps	22
major rules	3
active labels	cnf andrules