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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [not](x0) = x0,
     
     [and](x0, x1) = x0 + x1,
     
     [or](x0, x1) = x0 + x1 + 1
    orientation:
     or(x,x) = 2x + 1 >= x = x
     
     and(x,x) = 2x >= x = x
     
     not(not(x)) = x >= x = x
     
     not(and(x,y)) = x + y >= x + y + 1 = or(not(x),not(y))
     
     not(or(x,y)) = x + y + 1 >= x + y = and(not(x),not(y))
    problem:
     strict:
      and(x,x) -> x
      not(not(x)) -> x
      not(and(x,y)) -> or(not(x),not(y))
     weak:
      or(x,x) -> x
      not(or(x,y)) -> and(not(x),not(y))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [not](x0) = x0 + 1,
       
       [and](x0, x1) = x0 + x1,
       
       [or](x0, x1) = x0 + x1 + 1
      orientation:
       and(x,x) = 2x >= x = x
       
       not(not(x)) = x + 2 >= x = x
       
       not(and(x,y)) = x + y + 1 >= x + y + 3 = or(not(x),not(y))
       
       or(x,x) = 2x + 1 >= x = x
       
       not(or(x,y)) = x + y + 2 >= x + y + 2 = and(not(x),not(y))
      problem:
       strict:
        and(x,x) -> x
        not(and(x,y)) -> or(not(x),not(y))
       weak:
        not(not(x)) -> x
        or(x,x) -> x
        not(or(x,y)) -> and(not(x),not(y))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [not](x0) = x0,
         
         [and](x0, x1) = x0 + x1 + 1,
         
         [or](x0, x1) = x0 + x1 + 1
        orientation:
         and(x,x) = 2x + 1 >= x = x
         
         not(and(x,y)) = x + y + 1 >= x + y + 1 = or(not(x),not(y))
         
         not(not(x)) = x >= x = x
         
         or(x,x) = 2x + 1 >= x = x
         
         not(or(x,y)) = x + y + 1 >= x + y + 1 = and(not(x),not(y))
        problem:
         strict:
          not(and(x,y)) -> or(not(x),not(y))
         weak:
          and(x,x) -> x
          not(not(x)) -> x
          or(x,x) -> x
          not(or(x,y)) -> and(not(x),not(y))
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                       [1 1]  
           [not](x0) = [0 1]x0,
           
                           [1 1]          [0]
           [and](x0, x1) = [0 1]x0 + x1 + [1],
           
                          [1 1]          [0]
           [or](x0, x1) = [0 1]x0 + x1 + [1]
          orientation:
                           [1 2]    [1 1]    [1]    [1 2]    [1 1]    [0]                    
           not(and(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = or(not(x),not(y))
           
                      [2 1]    [0]         
           and(x,x) = [0 2]x + [1] >= x = x
           
                         [1 2]          
           not(not(x)) = [0 1]x >= x = x
           
                     [2 1]    [0]         
           or(x,x) = [0 2]x + [1] >= x = x
           
                          [1 2]    [1 1]    [1]    [1 2]    [1 1]    [0]                     
           not(or(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = and(not(x),not(y))
          problem:
           strict:
            
           weak:
            not(and(x,y)) -> or(not(x),not(y))
            and(x,x) -> x
            not(not(x)) -> x
            or(x,x) -> x
            not(or(x,y)) -> and(not(x),not(y))
          Qed