Exercise logic.propositional.dnf
Description
Proposition to DNF
All applications
Rule | compland.sort |
Location | [0] |
(~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | compland.sort |
Location | [0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [] |
F || (~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r || F
ready: no
Rule | falsezeroor.inv |
Location | [0] |
F || (~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || F || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0] |
((F || ~(q -> r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0] |
((~(q -> r) || F) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0] |
(~(F || (q -> r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0] |
(~((q -> r) || F) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0] |
(~((F || q) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,0] |
(~((q || F) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1] |
(~(q -> (F || r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,0,0,1] |
(~(q -> (r || F)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1] |
(~(q -> r) /\ (F || (~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)))) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1] |
(~(q -> r) /\ ((~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || F)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0] |
(~(q -> r) /\ (F || ~((q /\ T) -> r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0] |
(~(q -> r) /\ (~((q /\ T) -> r) || F) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0] |
(~(q -> r) /\ ~(F || ((q /\ T) -> r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0] |
(~(q -> r) /\ ~(((q /\ T) -> r) || F) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~((F || (q /\ T)) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~(((q /\ T) || F) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,0,0] |
(~(q -> r) /\ ~(((F || q) /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,0,0] |
(~(q -> r) /\ ~(((q || F) /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ (F || T)) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ (T || F)) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> (F || r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> (r || F)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ (F || (~(q -> r) /\ ~((q /\ T) -> r)))) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ((~(q -> r) /\ ~((q /\ T) -> r)) || F)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ (F || ~(q -> r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ (~(q -> r) || F) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(F || (q -> r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q -> r) || F) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((F || q) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q || F) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> (F || r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> (r || F)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ (F || ~((q /\ T) -> r))) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ (~((q /\ T) -> r) || F)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(F || ((q /\ T) -> r))) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q /\ T) -> r) || F)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((F || (q /\ T)) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q /\ T) || F) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((F || q) /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q || F) /\ T) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ (F || T)) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ (T || F)) -> r)) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> (F || r))) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [0,1,1,1,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> (r || F))) || q || r
ready: no
Rule | falsezeroor.inv |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || F || q || r
ready: no
Rule | falsezeroor.inv |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r || F
ready: no
Rule | falsezeroor.inv |
Location | [1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || F || q || r
ready: no
Rule | falsezeroor.inv |
Location | [1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || F || r
ready: no
Rule | falsezeroor.inv |
Location | [1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || F || r
ready: no
Rule | falsezeroor.inv |
Location | [1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r || F
ready: no
Rule | idempand.inv |
Location | [] |
((~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r) /\ ((~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r)
ready: no
Rule | idempand.inv |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,0] |
(~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,0,0] |
(~((q -> r) /\ (q -> r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,0,0,0] |
(~((q /\ q) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,0,0,1] |
(~(q -> (r /\ r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,0,0] |
(~(q -> r) /\ ~(((q /\ T) -> r) /\ ((q /\ T) -> r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T /\ q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,0,0,0,0] |
(~(q -> r) /\ ~((q /\ q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ T /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> (r /\ r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q -> r) /\ (q -> r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ q) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> (r /\ r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q /\ T) -> r) /\ ((q /\ T) -> r))) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T /\ q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ q /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T /\ T) -> r)) || q || r
ready: no
Rule | idempand.inv |
Location | [0,1,1,1,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> (r /\ r))) || q || r
ready: no
Rule | idempand.inv |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || ((q || r) /\ (q || r))
ready: no
Rule | idempand.inv |
Location | [1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || (q /\ q) || r
ready: no
Rule | idempand.inv |
Location | [1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || (r /\ r)
ready: no
Rule | idempor.inv |
Location | [] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r || (~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || (~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,0] |
((~(q -> r) || ~(q -> r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,0,0] |
(~((q -> r) || (q -> r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,0,0,0] |
(~((q || q) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,0,0,1] |
(~(q -> (r || r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1] |
(~(q -> r) /\ ((~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || (~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)))) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,0] |
(~(q -> r) /\ (~((q /\ T) -> r) || ~((q /\ T) -> r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,0,0] |
(~(q -> r) /\ ~(((q /\ T) -> r) || ((q /\ T) -> r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~(((q /\ T) || (q /\ T)) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,0,0,0,0] |
(~(q -> r) /\ ~(((q || q) /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ (T || T)) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> (r || r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ((~(q -> r) /\ ~((q /\ T) -> r)) || (~(q -> r) /\ ~((q /\ T) -> r)))) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ (~(q -> r) || ~(q -> r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q -> r) || (q -> r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q || q) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> (r || r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ (~((q /\ T) -> r) || ~((q /\ T) -> r))) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q /\ T) -> r) || ((q /\ T) -> r))) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q /\ T) || (q /\ T)) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q || q) /\ T) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ (T || T)) -> r)) || q || r
ready: no
Rule | idempor.inv |
Location | [0,1,1,1,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> (r || r))) || q || r
ready: no
Rule | idempor.inv |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r || q || r
ready: no
Rule | idempor.inv |
Location | [1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || q || r
ready: no
Rule | idempor.inv |
Location | [1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r || r
ready: no
Rule | logic.propositional.assocand |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.assocand |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.assocand |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.assocand |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.assocand |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.assocand |
Location | [0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.assocor |
Location | [] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.buggy.andsame |
Location | [0] |
Rule | logic.propositional.buggy.assoc |
Location | [] |
Rule | logic.propositional.buggy.assoc |
Location | [] |
Rule | logic.propositional.buggy.assoc |
Location | [] |
Rule | logic.propositional.buggy.assoc |
Location | [] |
Rule | logic.propositional.buggy.assoc |
Location | [] |
Rule | logic.propositional.buggy.assoc |
Location | [] |
Rule | logic.propositional.buggy.commimp |
Location | [0,0,0] |
Rule | logic.propositional.buggy.commimp |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.commimp |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.commimp |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1,1] |
Rule | logic.propositional.buggy.defimpl.inv |
Location | [0,1,1] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.demorgan3.inv |
Location | [0,1,1] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr |
Location | [] |
Rule | logic.propositional.buggy.distr.inv |
Location | [0] |
Rule | logic.propositional.buggy.distr.inv |
Location | [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 | [0,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,0,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,0,0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,1,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,1,0,0,0] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,1,0,0,1] |
Rule | logic.propositional.buggy.idemequiv.inv |
Location | [0,1,1,1,0,1] |
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,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,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,0,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,0,0,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,0,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,0,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,1,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,1,0,0,0] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,1,0,0,1] |
Rule | logic.propositional.buggy.idemimp.inv |
Location | [0,1,1,1,0,1] |
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,1] |
Rule | logic.propositional.buggy.implelim |
Location | [0,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.implelim |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.implelim1 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.implelim1 |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.implelim1 |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.implelim1 |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.implelim2 |
Location | [0,0,0] |
Rule | logic.propositional.buggy.implelim2 |
Location | [0,1,0,0] |
Rule | logic.propositional.buggy.implelim2 |
Location | [0,1,1,0,0] |
Rule | logic.propositional.buggy.implelim2 |
Location | [0,1,1,1,0] |
Rule | logic.propositional.buggy.notoverimpl |
Location | [0,0] |
Rule | logic.propositional.buggy.notoverimpl |
Location | [0,1,0] |
Rule | logic.propositional.buggy.notoverimpl |
Location | [0,1,1,0] |
Rule | logic.propositional.buggy.notoverimpl |
Location | [0,1,1,1] |
Rule | logic.propositional.buggy.trueprop |
Location | [0,1,0,0,0] |
Rule | logic.propositional.buggy.trueprop |
Location | [0,1,1,1,0,0] |
Rule | logic.propositional.command |
Location | [0] |
(~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~((q /\ T) -> r) /\ ~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~((q /\ T) -> r) /\ ~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0] |
(~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0,1] |
(~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0,1] |
(~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~((T /\ q) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | logic.propositional.command |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((T /\ q) -> r)) || q || r
ready: no
Rule | logic.propositional.commor |
Location | [] |
q || r || (~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r))
ready: no
Rule | logic.propositional.commor |
Location | [] |
r || (~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q
ready: no
Rule | logic.propositional.commor |
Location | [] |
q || (~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || r
ready: no
Rule | logic.propositional.commor |
Location | [] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || r || q
ready: no
Rule | logic.propositional.commor |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || r || q
ready: no
Rule | logic.propositional.defimpl |
Location | [0,0,0] |
(~(~q || r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.defimpl |
Location | [0,1,0,0] |
(~(q -> r) /\ ~(~(q /\ T) || r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.defimpl |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(~q || r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.defimpl |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(~(q /\ T) || r)) || q || r
ready: no
Rule | logic.propositional.genoroverand |
Location | [] |
(~(q -> r) || q || r) /\ (~((q /\ T) -> r) || q || r) /\ (~(q -> r) || q || r) /\ (~((q /\ T) -> r) || q || r)
ready: no
Rule | logic.propositional.genoroverand |
Location | [] |
(~(q -> r) || q || r) /\ (~((q /\ T) -> r) || q || r) /\ ((~(q -> r) /\ ~((q /\ T) -> r)) || q || r)
ready: no
Rule | logic.propositional.genoroverand |
Location | [] |
(~(q -> r) || q || r) /\ ((~((q /\ T) -> r) /\ ~(q -> r)) || q || r) /\ (~((q /\ T) -> r) || q || r)
ready: no
Rule | logic.propositional.genoroverand |
Location | [] |
((~(q -> r) /\ ~((q /\ T) -> r)) || q || r) /\ (~(q -> r) || q || r) /\ (~((q /\ T) -> r) || q || r)
ready: no
Rule | logic.propositional.idempand |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.invdemorganor |
Location | [0] |
~((q -> r) || ((q /\ T) -> r) || (q -> r) || ((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.invdemorganor |
Location | [0,1] |
(~(q -> r) /\ ~(((q /\ T) -> r) || (q -> r) || ((q /\ T) -> r))) || q || r
ready: no
Rule | logic.propositional.invdemorganor |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q -> r) || ((q /\ T) -> r))) || q || r
ready: no
Rule | logic.propositional.oroverand |
Location | [] |
(~(q -> r) || q || r) /\ ((~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r)
ready: no
Rule | logic.propositional.oroverand |
Location | [] |
((~(q -> r) /\ ~((q /\ T) -> r)) || q || r) /\ ((~(q -> r) /\ ~((q /\ T) -> r)) || q || r)
ready: no
Rule | logic.propositional.oroverand |
Location | [] |
((~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q || r) /\ (~((q /\ T) -> r) || q || r)
ready: no
Rule | logic.propositional.oroverand |
Location | [] |
((~(q -> r) || q) /\ ((~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q)) || r
ready: no
Rule | logic.propositional.oroverand |
Location | [] |
(((~(q -> r) /\ ~((q /\ T) -> r)) || q) /\ ((~(q -> r) /\ ~((q /\ T) -> r)) || q)) || r
ready: no
Rule | logic.propositional.oroverand |
Location | [] |
(((~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r)) || q) /\ (~((q /\ T) -> r) || q)) || r
ready: no
Rule | logic.propositional.truezeroand |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~(q -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | logic.propositional.truezeroand |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(q -> r)) || q || r
ready: no
Rule | notfalse.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ ~F) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notfalse.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ ~F) -> r)) || q || r
ready: no
~~((~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r)
ready: no
Rule | notnot.inv |
Location | [0] |
~~(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,0] |
(~~~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,0,0] |
(~~~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,0,0,0] |
(~(~~q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,0,0,1] |
(~(q -> ~~r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1] |
(~(q -> r) /\ ~~(~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r))) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,0] |
(~(q -> r) /\ ~~~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,0,0] |
(~(q -> r) /\ ~~~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~(~~(q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,0,0,0,0] |
(~(q -> r) /\ ~((~~q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ ~~T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> ~~r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~~(~(q -> r) /\ ~((q /\ T) -> r))) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~~~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~~~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(~~q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> ~~r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~~~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~~~((q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(~~(q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((~~q /\ T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ ~~T) -> r)) || q || r
ready: no
Rule | notnot.inv |
Location | [0,1,1,1,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> ~~r)) || q || r
ready: no
Rule | notnot.inv |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || ~~(q || r)
ready: no
Rule | notnot.inv |
Location | [1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || ~~q || r
ready: no
Rule | notnot.inv |
Location | [1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || ~~r
ready: no
Rule | truezeroand.inv |
Location | [] |
T /\ ((~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r)
ready: no
Rule | truezeroand.inv |
Location | [] |
((~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r) /\ T
ready: no
Rule | truezeroand.inv |
Location | [0] |
(T /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ T) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0] |
(T /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0] |
(~(q -> r) /\ T /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0,0] |
(~(T /\ (q -> r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0,0] |
(~((q -> r) /\ T) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0] |
(~((T /\ q) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,0] |
(~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1] |
(~(q -> (T /\ r)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,0,0,1] |
(~(q -> (r /\ T)) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1] |
(~(q -> r) /\ T /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ T) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0] |
(~(q -> r) /\ T /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ T /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0] |
(~(q -> r) /\ ~(T /\ ((q /\ T) -> r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0] |
(~(q -> r) /\ ~(((q /\ T) -> r) /\ T) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~((T /\ q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,0,0] |
(~(q -> r) /\ ~((T /\ q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,0,0] |
(~(q -> r) /\ ~((q /\ T /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ T /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,0,1] |
(~(q -> r) /\ ~((q /\ T /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> (T /\ r)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> (r /\ T)) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ T /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ T) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ T /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ T /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(T /\ (q -> r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q -> r) /\ T) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((T /\ q) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> (T /\ r)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> (r /\ T)) /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ T /\ ~((q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r) /\ T) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(T /\ ((q /\ T) -> r))) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~(((q /\ T) -> r) /\ T)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((T /\ q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((T /\ q /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,0,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T /\ T) -> r)) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> (T /\ r))) || q || r
ready: no
Rule | truezeroand.inv |
Location | [0,1,1,1,0,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> (r /\ T))) || q || r
ready: no
Rule | truezeroand.inv |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || (T /\ (q || r))
ready: no
Rule | truezeroand.inv |
Location | [1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || ((q || r) /\ T)
ready: no
Rule | truezeroand.inv |
Location | [1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || (T /\ q) || r
ready: no
Rule | truezeroand.inv |
Location | [1,0] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || (q /\ T) || r
ready: no
Rule | truezeroand.inv |
Location | [1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || (T /\ r)
ready: no
Rule | truezeroand.inv |
Location | [1,1] |
(~(q -> r) /\ ~((q /\ T) -> r) /\ ~(q -> r) /\ ~((q /\ T) -> r)) || q || (r /\ T)
ready: no