YES(?,O(n^2))

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:
 RT Transformation Processor:
  strict:
   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))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [not](x0) = x0,
    
    [and](x0, x1) = x0 + x1 + 8,
    
    [or](x0, x1) = x0 + x1 + 11
   orientation:
    or(x,x) = 2x + 11 >= x = x
    
    and(x,x) = 2x + 8 >= x = x
    
    not(not(x)) = x >= x = x
    
    not(and(x,y)) = x + y + 8 >= x + y + 11 = or(not(x),not(y))
    
    not(or(x,y)) = x + y + 11 >= x + y + 8 = and(not(x),not(y))
   problem:
    strict:
     not(not(x)) -> x
     not(and(x,y)) -> or(not(x),not(y))
    weak:
     or(x,x) -> x
     and(x,x) -> x
     not(or(x,y)) -> and(not(x),not(y))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [not](x0) = x0 + 8,
     
     [and](x0, x1) = x0 + x1 + 8,
     
     [or](x0, x1) = x0 + x1 + 16
    orientation:
     not(not(x)) = x + 16 >= x = x
     
     not(and(x,y)) = x + y + 16 >= x + y + 32 = or(not(x),not(y))
     
     or(x,x) = 2x + 16 >= x = x
     
     and(x,x) = 2x + 8 >= x = x
     
     not(or(x,y)) = x + y + 24 >= x + y + 24 = and(not(x),not(y))
    problem:
     strict:
      not(and(x,y)) -> or(not(x),not(y))
     weak:
      not(not(x)) -> x
      or(x,x) -> x
      and(x,x) -> x
      not(or(x,y)) -> and(not(x),not(y))
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                  [1 1]     [8]
      [not](x0) = [0 1]x0 + [0],
      
                      [1 2]          [9]
      [and](x0, x1) = [0 1]x0 + x1 + [9],
      
                     [1 2]          [8]
      [or](x0, x1) = [0 1]x0 + x1 + [9]
     orientation:
                      [1 3]    [1 1]    [26]    [1 3]    [1 1]    [24]                    
      not(and(x,y)) = [0 1]x + [0 1]y + [9 ] >= [0 1]x + [0 1]y + [9 ] = or(not(x),not(y))
      
                    [1 2]    [16]         
      not(not(x)) = [0 1]x + [0 ] >= x = x
      
                [2 2]    [8]         
      or(x,x) = [0 2]x + [9] >= x = x
      
                 [2 2]    [9]         
      and(x,x) = [0 2]x + [9] >= x = x
      
                     [1 3]    [1 1]    [25]    [1 3]    [1 1]    [25]                     
      not(or(x,y)) = [0 1]x + [0 1]y + [9 ] >= [0 1]x + [0 1]y + [9 ] = and(not(x),not(y))
     problem:
      strict:
       
      weak:
       not(and(x,y)) -> or(not(x),not(y))
       not(not(x)) -> x
       or(x,x) -> x
       and(x,x) -> x
       not(or(x,y)) -> and(not(x),not(y))
     Qed