Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

((T /\ p) || (~q /\ ~~(p /\ T /\ ~~~q) /\ ~(T /\ F) /\ T /\ p /\ ~r)) /\ ~~~~(p /\ ~q) /\ ~F /\ ~~T /\ p /\ T /\ (~F || (~q /\ ~~(p /\ ~~~q) /\ ~F /\ T /\ p /\ ~r)) /\ ~q /\ T /\ ((~q /\ ~(~p || ~~q)) || (~q /\ ~~(p /\ ~~~q) /\ ~F /\ p /\ ~r)) /\ (q || (~q /\ ~~(p /\ ~~~q) /\ ~F /\ T /\ p /\ ~r)) /\ (T || (~q /\ ~~(p /\ ~~~q) /\ ~F /\ T /\ p /\ ~r))

ready: no

Feedback

(no onefirst)
allfirsts (0)
allapplications
derivation
microsteps

Path 1

path [0, 2, 0, 0, 0, 1, 0, 0, 0, 0, 0, 3]
steps 12
major rules 2
active labels
dnf
orrules

enter dnf, check, navigator.down, check, enter simplify, enter andrules, logic.propositional.falsezeroand, exit andrules, exit simplify, navigator.up, enter orrules, logic.propositional.absorpor

path	[0, 2, 0, 0, 0, 1, 0, 0, 0, 0, 0, 3]
steps	12
major rules	2
active labels	dnf orrules