YES

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

Proof:
 DP Processor:
  DPs:
   not#(and(x,y)) -> not#(y)
   not#(and(x,y)) -> not#(x)
   not#(and(x,y)) -> or#(not(x),not(y))
   not#(or(x,y)) -> not#(y)
   not#(or(x,y)) -> not#(x)
   not#(or(x,y)) -> and#(not(x),not(y))
  TRS:
   or(x,x) -> x
   and(x,x) -> x
   not(not(x)) -> x
   not(and(x,y)) -> or(not(x),not(y))
   not(or(x,y)) -> and(not(x),not(y))
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    
   interpretation:
    [not#](x0) = x0,
    
    [and#](x0, x1) = 0,
    
    [or#](x0, x1) = 1,
    
    [not](x0) = x0 + 2,
    
    [and](x0, x1) = 2x0 + 1x1 + 7,
    
    [or](x0, x1) = 1x0 + 1x1 + 1
   orientation:
    not#(and(x,y)) = 2x + 1y + 7 >= y = not#(y)
    
    not#(and(x,y)) = 2x + 1y + 7 >= x = not#(x)
    
    not#(and(x,y)) = 2x + 1y + 7 >= 1 = or#(not(x),not(y))
    
    not#(or(x,y)) = 1x + 1y + 1 >= y = not#(y)
    
    not#(or(x,y)) = 1x + 1y + 1 >= x = not#(x)
    
    not#(or(x,y)) = 1x + 1y + 1 >= 0 = and#(not(x),not(y))
    
    or(x,x) = 1x + 1 >= x = x
    
    and(x,x) = 2x + 7 >= x = x
    
    not(not(x)) = x + 2 >= x = x
    
    not(and(x,y)) = 2x + 1y + 7 >= 1x + 1y + 3 = or(not(x),not(y))
    
    not(or(x,y)) = 1x + 1y + 2 >= 2x + 1y + 7 = and(not(x),not(y))
   problem:
    DPs:
     
    TRS:
     or(x,x) -> x
     and(x,x) -> x
     not(not(x)) -> x
     not(and(x,y)) -> or(not(x),not(y))
     not(or(x,y)) -> and(not(x),not(y))
   Qed