YES(?,O(n^2))

Problem:
 i(0()) -> 0()
 +(0(),y) -> y
 +(x,0()) -> x
 i(i(x)) -> x
 +(i(x),x) -> 0()
 +(x,i(x)) -> 0()
 i(+(x,y)) -> +(i(x),i(y))
 +(x,+(y,z)) -> +(+(x,y),z)
 +(+(x,i(y)),y) -> x
 +(+(x,y),i(y)) -> x

Proof:
 Complexity Transformation Processor:
  strict:
   i(0()) -> 0()
   +(0(),y) -> y
   +(x,0()) -> x
   i(i(x)) -> x
   +(i(x),x) -> 0()
   +(x,i(x)) -> 0()
   i(+(x,y)) -> +(i(x),i(y))
   +(x,+(y,z)) -> +(+(x,y),z)
   +(+(x,i(y)),y) -> x
   +(+(x,y),i(y)) -> x
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [+](x0, x1) = x0 + x1 + 1,
     
     [i](x0) = x0,
     
     [0] = 0
    orientation:
     i(0()) = 0 >= 0 = 0()
     
     +(0(),y) = y + 1 >= y = y
     
     +(x,0()) = x + 1 >= x = x
     
     i(i(x)) = x >= x = x
     
     +(i(x),x) = 2x + 1 >= 0 = 0()
     
     +(x,i(x)) = 2x + 1 >= 0 = 0()
     
     i(+(x,y)) = x + y + 1 >= x + y + 1 = +(i(x),i(y))
     
     +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z)
     
     +(+(x,i(y)),y) = x + 2y + 2 >= x = x
     
     +(+(x,y),i(y)) = x + 2y + 2 >= x = x
    problem:
     strict:
      i(0()) -> 0()
      i(i(x)) -> x
      i(+(x,y)) -> +(i(x),i(y))
      +(x,+(y,z)) -> +(+(x,y),z)
     weak:
      +(0(),y) -> y
      +(x,0()) -> x
      +(i(x),x) -> 0()
      +(x,i(x)) -> 0()
      +(+(x,i(y)),y) -> x
      +(+(x,y),i(y)) -> x
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [+](x0, x1) = x0 + x1,
       
       [i](x0) = x0 + 1,
       
       [0] = 0
      orientation:
       i(0()) = 1 >= 0 = 0()
       
       i(i(x)) = x + 2 >= x = x
       
       i(+(x,y)) = x + y + 1 >= x + y + 2 = +(i(x),i(y))
       
       +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
       
       +(0(),y) = y >= y = y
       
       +(x,0()) = x >= x = x
       
       +(i(x),x) = 2x + 1 >= 0 = 0()
       
       +(x,i(x)) = 2x + 1 >= 0 = 0()
       
       +(+(x,i(y)),y) = x + 2y + 1 >= x = x
       
       +(+(x,y),i(y)) = x + 2y + 1 >= x = x
      problem:
       strict:
        i(+(x,y)) -> +(i(x),i(y))
        +(x,+(y,z)) -> +(+(x,y),z)
       weak:
        i(0()) -> 0()
        i(i(x)) -> x
        +(0(),y) -> y
        +(x,0()) -> x
        +(i(x),x) -> 0()
        +(x,i(x)) -> 0()
        +(+(x,i(y)),y) -> x
        +(+(x,y),i(y)) -> x
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                            [1 1]     [0]
         [+](x0, x1) = x0 + [0 1]x1 + [1],
         
                     
         [i](x0) = x0,
         
               [0]
         [0] = [0]
        orientation:
                         [1 1]    [0]        [1 1]    [0]               
         i(+(x,y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = +(i(x),i(y))
         
                           [1 1]    [1 2]    [1]        [1 1]    [1 1]    [0]              
         +(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z)
         
                  [0]    [0]      
         i(0()) = [0] >= [0] = 0()
         
                             
         i(i(x)) = x >= x = x
         
                    [1 1]    [0]         
         +(0(),y) = [0 1]y + [1] >= y = y
         
                        [0]         
         +(x,0()) = x + [1] >= x = x
         
                     [2 1]    [0]    [0]      
         +(i(x),x) = [0 2]x + [1] >= [0] = 0()
         
                     [2 1]    [0]    [0]      
         +(x,i(x)) = [0 2]x + [1] >= [0] = 0()
         
                              [2 2]    [0]         
         +(+(x,i(y)),y) = x + [0 2]y + [2] >= x = x
         
                              [2 2]    [0]         
         +(+(x,y),i(y)) = x + [0 2]y + [2] >= x = x
        problem:
         strict:
          i(+(x,y)) -> +(i(x),i(y))
         weak:
          +(x,+(y,z)) -> +(+(x,y),z)
          i(0()) -> 0()
          i(i(x)) -> x
          +(0(),y) -> y
          +(x,0()) -> x
          +(i(x),x) -> 0()
          +(x,i(x)) -> 0()
          +(+(x,i(y)),y) -> x
          +(+(x,y),i(y)) -> x
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                                   [0]
           [+](x0, x1) = x0 + x1 + [1],
           
                     [1 1]  
           [i](x0) = [0 1]x0,
           
                 [0]
           [0] = [0]
          orientation:
                       [1 1]    [1 1]    [1]    [1 1]    [1 1]    [0]               
           i(+(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = +(i(x),i(y))
           
                                     [0]                [0]              
           +(x,+(y,z)) = x + y + z + [2] >= x + y + z + [2] = +(+(x,y),z)
           
                    [0]    [0]      
           i(0()) = [0] >= [0] = 0()
           
                     [1 2]          
           i(i(x)) = [0 1]x >= x = x
           
                          [0]         
           +(0(),y) = y + [1] >= y = y
           
                          [0]         
           +(x,0()) = x + [1] >= x = x
           
                       [2 1]    [0]    [0]      
           +(i(x),x) = [0 2]x + [1] >= [0] = 0()
           
                       [2 1]    [0]    [0]      
           +(x,i(x)) = [0 2]x + [1] >= [0] = 0()
           
                                [2 1]    [0]         
           +(+(x,i(y)),y) = x + [0 2]y + [2] >= x = x
           
                                [2 1]    [0]         
           +(+(x,y),i(y)) = x + [0 2]y + [2] >= x = x
          problem:
           strict:
            
           weak:
            i(+(x,y)) -> +(i(x),i(y))
            +(x,+(y,z)) -> +(+(x,y),z)
            i(0()) -> 0()
            i(i(x)) -> x
            +(0(),y) -> y
            +(x,0()) -> x
            +(i(x),x) -> 0()
            +(x,i(x)) -> 0()
            +(+(x,i(y)),y) -> x
            +(+(x,y),i(y)) -> x
          Qed