Exercise logic.propositional.dnf
Description
Proposition to DNF
All applications
Rule | falsezeroor.inv |
Location | [] |
F || ~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) || F
ready: no
Rule | falsezeroor.inv |
Location | [0] |
~(F || ~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | falsezeroor.inv |
Location | [0] |
~(~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) || F)
ready: no
Rule | falsezeroor.inv |
Location | [0,0] |
~~(F || (((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0] |
~~((((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) || F)
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0] |
~~((F || ((~p /\ ~p) <-> (p /\ q))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0] |
~~((((~p /\ ~p) <-> (p /\ q)) || F) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0] |
~~(((F || (~p /\ ~p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0] |
~~((((~p /\ ~p) || F) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,0] |
~~((((F || ~p) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,0] |
~~((((~p || F) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,0,0] |
~~(((~(F || p) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,0,0] |
~~(((~(p || F) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,1] |
~~(((~p /\ (F || ~p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,1] |
~~(((~p /\ (~p || F)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,1,0] |
~~(((~p /\ ~(F || p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0,1,0] |
~~(((~p /\ ~(p || F)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> (F || (p /\ q))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> ((p /\ q) || F)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1,0] |
~~(((~p /\ ~p) <-> ((F || p) /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1,0] |
~~(((~p /\ ~p) <-> ((p || F) /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ (F || q))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ (q || F))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (F || ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (((~p /\ ~p) <-> (p /\ q)) || F))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((F || (~p /\ ~p)) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (((~p /\ ~p) || F) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (((F || ~p) /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (((~p || F) /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~(F || p) /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~(p || F) /\ ~p) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ (F || ~p)) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ (~p || F)) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~(F || p)) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~(p || F)) <-> (p /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (F || (p /\ q))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> ((p /\ q) || F)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> ((F || p) /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> ((p || F) /\ q)))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ (F || q))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,1,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ (q || F))))
ready: no
Rule | idempand.inv |
Location | [] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) /\ ~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0] |
~(~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) /\ ~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | idempand.inv |
Location | [0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,0] |
~~(((~p /\ ~p /\ ~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,0,0] |
~~(((~p /\ ~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,0,0,0] |
~~(((~(p /\ p) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,0,1] |
~~(((~p /\ ~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,0,1,0] |
~~(((~p /\ ~(p /\ p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q /\ p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p /\ ~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~(p /\ p) /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~(p /\ p)) <-> (p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q /\ p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ p /\ q)))
ready: no
Rule | idempand.inv |
Location | [0,0,1,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q /\ q)))
ready: no
Rule | idempor.inv |
Location | [] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) || ~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0] |
~(~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) || ~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | idempor.inv |
Location | [0,0] |
~~((((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) || (((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | idempor.inv |
Location | [0,0,0] |
~~((((~p /\ ~p) <-> (p /\ q)) || ((~p /\ ~p) <-> (p /\ q))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,0] |
~~((((~p /\ ~p) || (~p /\ ~p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,0,0] |
~~((((~p || ~p) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,0,0,0] |
~~(((~(p || p) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,0,1] |
~~(((~p /\ (~p || ~p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,0,1,0] |
~~(((~p /\ ~(p || p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> ((p /\ q) || (p /\ q))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,1,0] |
~~(((~p /\ ~p) <-> ((p || p) /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ (q || q))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (((~p /\ ~p) <-> (p /\ q)) || ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | idempor.inv |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (((~p /\ ~p) || (~p /\ ~p)) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,1,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (((~p || ~p) /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,1,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~(p || p) /\ ~p) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,1,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ (~p || ~p)) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,1,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~(p || p)) <-> (p /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> ((p /\ q) || (p /\ q))))
ready: no
Rule | idempor.inv |
Location | [0,0,1,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> ((p || p) /\ q)))
ready: no
Rule | idempor.inv |
Location | [0,0,1,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ (q || q))))
ready: no
Rule | logic.propositional.buggy.andsame |
Location | [0,0] |
Rule | logic.propositional.buggy.andsame |
Location | [0,0,0,0] |
Rule | logic.propositional.buggy.andsame |
Location | [0,0,1,0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,0,0,0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,0,0,0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,0,1,0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,0,1,0] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [0] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [0] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [0] |
Rule | logic.propositional.buggy.demorgan2 |
Location | [0] |
Rule | logic.propositional.buggy.demorgan3 |
Location | [0] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0,0,0,0] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0,0,1,0] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim1 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim2 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim2 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim2 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim2 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim2 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim2 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.equivelim3 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.equivelim3 |
Location | [0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,0,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,0,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,1,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,0,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,0,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,0,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,0,1,1,1] |
Rule | logic.propositional.buggy.parenth1 |
Location | [0] |
Rule | logic.propositional.command |
Location | [0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.command |
Location | [0,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.command |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> (q /\ p)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.command |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.command |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (q /\ p)))
ready: no
Rule | logic.propositional.defequiv |
Location | [0,0,0] |
~~(((~p /\ ~p /\ p /\ q) || (~(~p /\ ~p) /\ ~(p /\ q))) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.defequiv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p /\ p /\ q) || (~(~p /\ ~p) /\ ~(p /\ q))))
ready: no
Rule | logic.propositional.demorganand |
Location | [0] |
~(~((~p /\ ~p) <-> (p /\ q)) || ~((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.idempand |
Location | [0,0] |
~~((~p /\ ~p) <-> (p /\ q))
ready: no
Rule | logic.propositional.idempand |
Location | [0,0,0,0] |
~~((~p <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.idempand |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (~p <-> (p /\ q)))
ready: no
Rule | logic.propositional.invdemorganor |
Location | [0,0,0,0] |
~~((~(p || p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.invdemorganor |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (~(p || p) <-> (p /\ q)))
ready: no
Rule | logic.propositional.notnot |
Location | [] |
((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))
ready: no
~~~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0] |
~~~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0] |
~~~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0] |
~~(~~((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,0] |
~~((~~(~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,0,0] |
~~(((~~~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,0,0,0] |
~~(((~~~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,0,1] |
~~(((~p /\ ~~~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,0,1,0] |
~~(((~p /\ ~~~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> ~~(p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,1,0] |
~~(((~p /\ ~p) <-> (~~p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ ~~q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ~~((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ (~~(~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~~~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~~~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~~~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~~~p) <-> (p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> ~~(p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (~~p /\ q)))
ready: no
Rule | notnot.inv |
Location | [0,0,1,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ ~~q)))
ready: no
Rule | truezeroand.inv |
Location | [] |
T /\ ~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) /\ T
ready: no
Rule | truezeroand.inv |
Location | [0] |
~(T /\ ~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))))
ready: no
Rule | truezeroand.inv |
Location | [0] |
~(~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q))) /\ T)
ready: no
Rule | truezeroand.inv |
Location | [0,0] |
~~(T /\ ((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)) /\ T)
ready: no
Rule | truezeroand.inv |
Location | [0,0,0] |
~~(T /\ ((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ T /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0] |
~~(((T /\ ~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0] |
~~(((~p /\ ~p /\ T) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,0] |
~~(((T /\ ~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,0] |
~~(((~p /\ T /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,0,0] |
~~(((~(T /\ p) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,0,0] |
~~(((~(p /\ T) /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,1] |
~~(((~p /\ T /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,1] |
~~(((~p /\ ~p /\ T) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,1,0] |
~~(((~p /\ ~(T /\ p)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0,1,0] |
~~(((~p /\ ~(p /\ T)) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> (T /\ p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q /\ T)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1,0] |
~~(((~p /\ ~p) <-> (T /\ p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ T /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ T /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q /\ T)) /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ T /\ ((~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q)) /\ T)
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((T /\ ~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p /\ T) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((T /\ ~p /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ T /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~(T /\ p) /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,0,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~(p /\ T) /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ T /\ ~p) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p /\ T) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~(T /\ p)) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,0,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~(p /\ T)) <-> (p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (T /\ p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q /\ T)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (T /\ p /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,1,0] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ T /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ T /\ q)))
ready: no
Rule | truezeroand.inv |
Location | [0,0,1,1,1] |
~~(((~p /\ ~p) <-> (p /\ q)) /\ ((~p /\ ~p) <-> (p /\ q /\ T)))
ready: no