Exercise logic.propositional.cnf

Description
Proposition to CNF

All applications

• Rule	falsezeroor.inv
  Location	[]

  

  F || (r -> q) || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[]

  

  (r -> q) || ~q || F

  ready: no

• Rule	falsezeroor.inv
  Location	[0]

  

  F || (r -> q) || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[0]

  

  (r -> q) || F || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[0,0]

  

  ((F || r) -> q) || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[0,0]

  

  ((r || F) -> q) || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[0,1]

  

  (r -> (F || q)) || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[0,1]

  

  (r -> (q || F)) || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[1]

  

  (r -> q) || F || ~q

  ready: no

• Rule	falsezeroor.inv
  Location	[1]

  

  (r -> q) || ~q || F

  ready: no

• Rule	falsezeroor.inv
  Location	[1,0]

  

  (r -> q) || ~(F || q)

  ready: no

• Rule	falsezeroor.inv
  Location	[1,0]

  

  (r -> q) || ~(q || F)

  ready: no

• Rule	idempand.inv
  Location	[]

  

  ((r -> q) || ~q) /\ ((r -> q) || ~q)

  ready: no

• Rule	idempand.inv
  Location	[0]

  

  ((r -> q) /\ (r -> q)) || ~q

  ready: no

• Rule	idempand.inv
  Location	[0,0]

  

  ((r /\ r) -> q) || ~q

  ready: no

• Rule	idempand.inv
  Location	[0,1]

  

  (r -> (q /\ q)) || ~q

  ready: no

• Rule	idempand.inv
  Location	[1]

  

  (r -> q) || (~q /\ ~q)

  ready: no

• Rule	idempand.inv
  Location	[1,0]

  

  (r -> q) || ~(q /\ q)

  ready: no

• Rule	idempor.inv
  Location	[]

  

  (r -> q) || ~q || (r -> q) || ~q

  ready: no

• Rule	idempor.inv
  Location	[0]

  

  (r -> q) || (r -> q) || ~q

  ready: no

• Rule	idempor.inv
  Location	[0,0]

  

  ((r || r) -> q) || ~q

  ready: no

• Rule	idempor.inv
  Location	[0,1]

  

  (r -> (q || q)) || ~q

  ready: no

• Rule	idempor.inv
  Location	[1]

  

  (r -> q) || ~q || ~q

  ready: no

• Rule	idempor.inv
  Location	[1,0]

  

  (r -> q) || ~(q || q)

  ready: no

• Rule	logic.propositional.buggy.commimp
  Location	[0]

• Rule	logic.propositional.buggy.defimpl.inv
  Location	[]

• 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,1]

• Rule	logic.propositional.buggy.idemequiv.inv
  Location	[1]

• Rule	logic.propositional.buggy.idemequiv.inv
  Location	[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,1]

• Rule	logic.propositional.buggy.idemimp.inv
  Location	[1]

• Rule	logic.propositional.buggy.idemimp.inv
  Location	[1,0]

• Rule	logic.propositional.buggy.implelim
  Location	[0]

• Rule	logic.propositional.buggy.implelim
  Location	[0]

• Rule	logic.propositional.buggy.implelim
  Location	[0]

• Rule	logic.propositional.buggy.implelim
  Location	[0]

• Rule	logic.propositional.buggy.implelim1
  Location	[0]

• Rule	logic.propositional.buggy.implelim2
  Location	[0]

• Rule	logic.propositional.commor
  Location	[]

  

  ~q || (r -> q)

  ready: no

• Rule	logic.propositional.defimpl
  Location	[0]

  

  ~r || q || ~q

  ready: yes

• Rule	notnot.inv
  Location	[]

  

  ~~((r -> q) || ~q)

  ready: no

• Rule	notnot.inv
  Location	[0]

  

  ~~(r -> q) || ~q

  ready: no

• Rule	notnot.inv
  Location	[0,0]

  

  (~~r -> q) || ~q

  ready: no

• Rule	notnot.inv
  Location	[0,1]

  

  (r -> ~~q) || ~q

  ready: no

• Rule	notnot.inv
  Location	[1]

  

  (r -> q) || ~~~q

  ready: no

• Rule	notnot.inv
  Location	[1,0]

  

  (r -> q) || ~~~q

  ready: no

• Rule	truezeroand.inv
  Location	[]

  

  T /\ ((r -> q) || ~q)

  ready: no

• Rule	truezeroand.inv
  Location	[]

  

  ((r -> q) || ~q) /\ T

  ready: no

• Rule	truezeroand.inv
  Location	[0]

  

  (T /\ (r -> q)) || ~q

  ready: no

• Rule	truezeroand.inv
  Location	[0]

  

  ((r -> q) /\ T) || ~q

  ready: no

• Rule	truezeroand.inv
  Location	[0,0]

  

  ((T /\ r) -> q) || ~q

  ready: no

• Rule	truezeroand.inv
  Location	[0,0]

  

  ((r /\ T) -> q) || ~q

  ready: no

• Rule	truezeroand.inv
  Location	[0,1]

  

  (r -> (T /\ q)) || ~q

  ready: no

• Rule	truezeroand.inv
  Location	[0,1]

  

  (r -> (q /\ T)) || ~q

  ready: no

• Rule	truezeroand.inv
  Location	[1]

  

  (r -> q) || (T /\ ~q)

  ready: no

• Rule	truezeroand.inv
  Location	[1]

  

  (r -> q) || (~q /\ T)

  ready: no

• Rule	truezeroand.inv
  Location	[1,0]

  

  (r -> q) || ~(T /\ q)

  ready: no

• Rule	truezeroand.inv
  Location	[1,0]

  

  (r -> q) || ~(q /\ T)

  ready: no