MAYBE

Problem:
 not(not(x)) -> x
 not(or(x,y)) -> and(not(x),not(y))
 not(and(x,y)) -> or(not(x),not(y))
 and(x,or(y,z)) -> or(and(x,y),and(x,z))
 and(or(y,z),x) -> or(and(x,y),and(x,z))

Proof:
 DP Processor:
  DPs:
   not#(or(x,y)) -> not#(y)
   not#(or(x,y)) -> not#(x)
   not#(or(x,y)) -> and#(not(x),not(y))
   not#(and(x,y)) -> not#(y)
   not#(and(x,y)) -> not#(x)
   and#(x,or(y,z)) -> and#(x,z)
   and#(x,or(y,z)) -> and#(x,y)
   and#(or(y,z),x) -> and#(x,z)
   and#(or(y,z),x) -> and#(x,y)
  TRS:
   not(not(x)) -> x
   not(or(x,y)) -> and(not(x),not(y))
   not(and(x,y)) -> or(not(x),not(y))
   and(x,or(y,z)) -> or(and(x,y),and(x,z))
   and(or(y,z),x) -> or(and(x,y),and(x,z))
  Open