Exercise logic.propositional.dnf
Description
Proposition to DNF
All applications
Rule | defimpl.inv |
Location | [] |
~p -> ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [] |
F || ~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))) || F
ready: no
Rule | falsezeroor.inv |
Location | [0] |
F || ~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [0] |
~~p || F || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0] |
~(F || ~p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0] |
~(~p || F) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0] |
~~(F || p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0] |
~~(p || F) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1] |
~~p || F || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))) || F
ready: no
Rule | falsezeroor.inv |
Location | [1,0] |
~~p || ((F || F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0] |
~~p || ((F || (q /\ ~(T /\ ~T)) || F) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,0] |
~~p || ((F || F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,0] |
~~p || ((F || F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1] |
~~p || ((F || F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T)) || F) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,0] |
~~p || ((F || ((F || q) /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,0] |
~~p || ((F || ((q || F) /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1] |
~~p || ((F || (q /\ (F || ~(T /\ ~T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1] |
~~p || ((F || (q /\ (~(T /\ ~T) || F))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~(F || (T /\ ~T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~((T /\ ~T) || F))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~((F || T) /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~((T || F) /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ (F || ~T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ (~T || F)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~(F || T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~(T || F)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (F || r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)) || F))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (F || r || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || F || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || F || (q /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)) || F))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || ((F || q) /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || ((q || F) /\ ~(T /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ (F || ~(T /\ ~T)))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ (~(T /\ ~T) || F))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(F || (T /\ ~T)))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~((T /\ ~T) || F))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~((F || T) /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~((T || F) /\ ~T))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ (F || ~T)))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ (~T || F)))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~(F || T)))))
ready: no
Rule | falsezeroor.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~(T || F)))))
ready: no
Rule | idempand.inv |
Location | [] |
(~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))) /\ (~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))))
ready: no
Rule | idempand.inv |
Location | [0] |
(~~p /\ ~~p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [0,0] |
~(~p /\ ~p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [0,0,0] |
~~(p /\ p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))) /\ (F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,0] |
~~p || (((F /\ F) || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T) /\ q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,1,0] |
~~p || ((F || (q /\ q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T) /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T /\ T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~(T /\ T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ ((r /\ r) || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T) /\ q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ q /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T) /\ ~(T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T /\ T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T /\ ~T))))
ready: no
Rule | idempand.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~(T /\ T)))))
ready: no
Rule | idempor.inv |
Location | [] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))) || ~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [0] |
~~p || ~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [0,0] |
~(~p || ~p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [0,0,0] |
~~(p || p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0] |
~~p || ((F || (q /\ ~(T /\ ~T)) || F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,0] |
~~p || ((F || F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T)) || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,1,0] |
~~p || ((F || ((q || q) /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,1,1] |
~~p || ((F || (q /\ (~(T /\ ~T) || ~(T /\ ~T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~((T /\ ~T) || (T /\ ~T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~((T || T) /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ (~T || ~T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~(T || T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)) || r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || r || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)) || (q /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || ((q || q) /\ ~(T /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ (~(T /\ ~T) || ~(T /\ ~T)))))
ready: no
Rule | idempor.inv |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~((T /\ ~T) || (T /\ ~T)))))
ready: no
Rule | idempor.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~((T || T) /\ ~T))))
ready: no
Rule | idempor.inv |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ (~T || ~T)))))
ready: no
Rule | idempor.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~(T || T)))))
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ r) || ((F || (q /\ ~(T /\ ~T))) /\ q /\ ~(T /\ ~T))
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
~~p || (F /\ (r || (q /\ ~(T /\ ~T)))) || (q /\ ~(T /\ ~T) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.buggy.andcompl |
Location | [1,0,1,1,0] |
Rule | logic.propositional.buggy.andcompl |
Location | [1,0,1,1,0] |
Rule | logic.propositional.buggy.andcompl |
Location | [1,1,1,1,0] |
Rule | logic.propositional.buggy.andcompl |
Location | [1,1,1,1,0] |
Rule | logic.propositional.buggy.assoc |
Location | [] |
Rule | logic.propositional.buggy.assoc |
Location | [1] |
Rule | logic.propositional.buggy.assoc |
Location | [1] |
Rule | logic.propositional.buggy.assoc |
Location | [1,0] |
Rule | logic.propositional.buggy.assoc |
Location | [1,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [1,0,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [1,0,1,1,0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [1,1,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [1,1,1,1,0] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.demorgan1 |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.demorgan2 |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.demorgan2 |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.demorgan3 |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.demorgan3 |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [1] |
Rule | logic.propositional.buggy.distr |
Location | [1] |
Rule | logic.propositional.buggy.distr |
Location | [1] |
Rule | logic.propositional.buggy.distr |
Location | [1] |
Rule | logic.propositional.buggy.distr |
Location | [1,0] |
Rule | logic.propositional.buggy.distr |
Location | [1,0] |
Rule | logic.propositional.buggy.distr |
Location | [1,1] |
Rule | logic.propositional.buggy.distr |
Location | [1,1] |
Rule | logic.propositional.buggy.distr.inv |
Location | [1] |
Rule | logic.propositional.buggy.distrnot |
Location | [] |
Rule | logic.propositional.buggy.distrnot |
Location | [] |
Rule | logic.propositional.buggy.falseprop |
Location | [1,0] |
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 | [1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,1,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,1,1,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,1,1,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,0,1,1,0,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,1,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,1,1,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,1,1,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [1,1,1,1,0,1,0] |
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 | [1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,1,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,1,1,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,1,1,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,0,1,1,0,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,1,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,1,1,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,1,1,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [1,1,1,1,0,1,0] |
Rule | logic.propositional.buggy.parenth1 |
Location | [1,0,1,1] |
Rule | logic.propositional.buggy.parenth1 |
Location | [1,1,1,1] |
Rule | logic.propositional.buggy.trueprop |
Location | [1,0,1,1,0] |
Rule | logic.propositional.buggy.trueprop |
Location | [1,1,1,1,0] |
Rule | logic.propositional.command |
Location | [1] |
~~p || ((r || (q /\ ~(T /\ ~T))) /\ (F || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.command |
Location | [1,0,1] |
~~p || ((F || (~(T /\ ~T) /\ q)) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.command |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~(~T /\ T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.command |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (~(T /\ ~T) /\ q)))
ready: no
Rule | logic.propositional.command |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(~T /\ T))))
ready: no
Rule | logic.propositional.commor |
Location | [] |
((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))) || ~~p
ready: no
Rule | logic.propositional.commor |
Location | [1,0] |
~~p || (((q /\ ~(T /\ ~T)) || F) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.commor |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ ((q /\ ~(T /\ ~T)) || r))
ready: no
Rule | logic.propositional.compland |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~F)) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.compland |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~F)))
ready: no
Rule | logic.propositional.demorganand |
Location | [1,0,1,1] |
~~p || ((F || (q /\ (~T || ~~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.demorganand |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ (~T || ~~T))))
ready: no
Rule | logic.propositional.falsezeroor |
Location | [1,0] |
~~p || (q /\ ~(T /\ ~T) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.invoroverand |
Location | [1] |
~~p || (F /\ r) || (q /\ ~(T /\ ~T))
ready: no
Rule | logic.propositional.notnot |
Location | [0] |
p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.nottrue |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ F))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.nottrue |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ F))))
ready: no
Rule | logic.propositional.oroverand |
Location | [] |
(~~p || F || (q /\ ~(T /\ ~T))) /\ (~~p || r || (q /\ ~(T /\ ~T)))
ready: no
Rule | logic.propositional.oroverand |
Location | [1,0] |
~~p || ((F || q) /\ (F || ~(T /\ ~T)) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.oroverand |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || q) /\ (r || ~(T /\ ~T)))
ready: no
Rule | logic.propositional.truezeroand |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~~T)) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | logic.propositional.truezeroand |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~~T)))
ready: no
Rule | notfalse.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~(~F /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notfalse.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~~F))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notfalse.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(~F /\ ~T))))
ready: no
Rule | notfalse.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~~F))))
ready: no
~~(~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))))
ready: no
Rule | notnot.inv |
Location | [0] |
~~~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [0,0] |
~~~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [0,0,0] |
~~~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1] |
~~p || ~~((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0] |
~~p || (~~(F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,0] |
~~p || ((~~F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,1] |
~~p || ((F || ~~(q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,1,0] |
~~p || ((F || (~~q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,1,1] |
~~p || ((F || (q /\ ~~~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~~~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~(~~T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~~~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~~~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ ~~(r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (~~r || (q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || ~~(q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (~~q /\ ~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~~~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~~~(T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(~~T /\ ~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~~~T))))
ready: no
Rule | notnot.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~~~T))))
ready: no
Rule | nottrue.inv |
Location | [1,0,0] |
~~p || ((~T || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | oroverand.inv |
Location | [1] |
~~p || (F /\ r) || (q /\ ~(T /\ ~T))
ready: no
Rule | truezeroand.inv |
Location | [] |
T /\ (~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T)))))
ready: no
Rule | truezeroand.inv |
Location | [] |
(~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))) /\ T
ready: no
Rule | truezeroand.inv |
Location | [0] |
(T /\ ~~p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [0] |
(~~p /\ T) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [0,0] |
~(T /\ ~p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [0,0] |
~(~p /\ T) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0] |
~~(T /\ p) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [0,0,0] |
~~(p /\ T) || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1] |
~~p || (T /\ (F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))) /\ T)
ready: no
Rule | truezeroand.inv |
Location | [1,0] |
~~p || (T /\ (F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ T /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,0] |
~~p || (((T /\ F) || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,0] |
~~p || (((F /\ T) || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1] |
~~p || ((F || (T /\ q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T) /\ T)) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,0] |
~~p || ((F || (T /\ q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,0] |
~~p || ((F || (q /\ T /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1] |
~~p || ((F || (q /\ T /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T) /\ T)) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~(T /\ T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T /\ T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T /\ T))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~(T /\ T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,0,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~(T /\ T)))) /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ T /\ (r || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T))) /\ T)
ready: no
Rule | truezeroand.inv |
Location | [1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ ((T /\ r) || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ ((r /\ T) || (q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (T /\ q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T) /\ T)))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (T /\ q /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ T /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ T /\ ~(T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T) /\ T)))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T /\ T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ T /\ ~T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0,1] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~T /\ T))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~(T /\ T)))))
ready: no
Rule | truezeroand.inv |
Location | [1,1,1,1,0,1,0] |
~~p || ((F || (q /\ ~(T /\ ~T))) /\ (r || (q /\ ~(T /\ ~(T /\ T)))))
ready: no