Exercise logic.propositional.dnf

Description
Proposition to DNF

All applications

• Rule	falsezeroor.inv
  Location	[]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[0,0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[0,0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[0,1]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[0,1]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,1]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,1]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,1,0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,1,0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,1,0,0]

  

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

  ready: no

• Rule	falsezeroor.inv
  Location	[1,1,0,0]

  

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

  ready: no

• Rule	idempand.inv
  Location	[]

  

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

  ready: no

• Rule	idempand.inv
  Location	[0]

  

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

  ready: no

• Rule	idempand.inv
  Location	[0,0]

  

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

  ready: no

• Rule	idempand.inv
  Location	[0,1]

  

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

  ready: no

• Rule	idempand.inv
  Location	[1]

  

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

  ready: no

• Rule	idempand.inv
  Location	[1,0]

  

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

  ready: no

• Rule	idempand.inv
  Location	[1,1]

  

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

  ready: no

• Rule	idempand.inv
  Location	[1,1,0]

  

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

  ready: no

• Rule	idempand.inv
  Location	[1,1,0,0]

  

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

  ready: no

• Rule	idempor.inv
  Location	[]

  

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

  ready: no

• Rule	idempor.inv
  Location	[0]

  

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

  ready: no

• Rule	idempor.inv
  Location	[0,0]

  

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

  ready: no

• Rule	idempor.inv
  Location	[0,1]

  

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

  ready: no

• Rule	idempor.inv
  Location	[1]

  

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

  ready: no

• Rule	idempor.inv
  Location	[1,0]

  

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

  ready: no

• Rule	idempor.inv
  Location	[1,1]

  

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

  ready: no

• Rule	idempor.inv
  Location	[1,1,0]

  

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

  ready: no

• Rule	idempor.inv
  Location	[1,1,0,0]

  

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

  ready: no

• Rule	logic.propositional.assocor
  Location	[]

  

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

  ready: no

• Rule	logic.propositional.buggy.assoc
  Location	[]

• Rule	logic.propositional.buggy.assoc
  Location	[]

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

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

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

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

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

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

• Rule	logic.propositional.command
  Location	[0]

  

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

  ready: no

• Rule	logic.propositional.commor
  Location	[]

  

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

  ready: no

• Rule	logic.propositional.commor
  Location	[]

  

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

  ready: no

• Rule	logic.propositional.commor
  Location	[]

  

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

  ready: no

• Rule	logic.propositional.commor
  Location	[]

  

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

  ready: no

• Rule	logic.propositional.commor
  Location	[1]

  

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

  ready: no

• Rule	logic.propositional.falsezeroand
  Location	[0]

  

  F || q || ~~p

  ready: no

• Rule	logic.propositional.notnot
  Location	[1,1]

  

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

  ready: yes

• Rule	logic.propositional.oroverand
  Location	[]

  

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

  ready: no

• Rule	logic.propositional.oroverand
  Location	[]

  

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

  ready: no

• Rule	notnot.inv
  Location	[]

  

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

  ready: no

• Rule	notnot.inv
  Location	[0]

  

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

  ready: no

• Rule	notnot.inv
  Location	[0,0]

  

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

  ready: no

• Rule	notnot.inv
  Location	[0,1]

  

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

  ready: no

• Rule	notnot.inv
  Location	[1]

  

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

  ready: no

• Rule	notnot.inv
  Location	[1,0]

  

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

  ready: no

• Rule	notnot.inv
  Location	[1,1]

  

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

  ready: no

• Rule	notnot.inv
  Location	[1,1,0]

  

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

  ready: no

• Rule	notnot.inv
  Location	[1,1,0,0]

  

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

  ready: no

• Rule	nottrue.inv
  Location	[0,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[0,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[0,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[0,1]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[0,1]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,1]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,1]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,1,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,1,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,1,0,0]

  

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

  ready: no

• Rule	truezeroand.inv
  Location	[1,1,0,0]

  

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

  ready: no