YES Problem: not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) Proof: DP Processor: DPs: not#(or(x,y)) -> not#(y) not#(or(x,y)) -> not#(not(y)) not#(or(x,y)) -> not#(not(not(y))) not#(or(x,y)) -> not#(x) not#(or(x,y)) -> not#(not(x)) not#(or(x,y)) -> not#(not(not(x))) not#(and(x,y)) -> not#(y) not#(and(x,y)) -> not#(not(y)) not#(and(x,y)) -> not#(not(not(y))) not#(and(x,y)) -> not#(x) not#(and(x,y)) -> not#(not(x)) not#(and(x,y)) -> not#(not(not(x))) TRS: not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) KBO Processor: argument filtering: pi(not) = [0] pi(or) = [0,1] pi(and) = [0,1] pi(not#) = 0 weight function: w0 = 1 w(not#) = 1 w(and) = w(or) = w(not) = 0 precedence: not# > not > and ~ or problem: DPs: TRS: not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) Qed