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:
 RT 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
   interpretation:
    [+](x0, x1) = x0 + x1 + 11,
    
    [i](x0) = x0 + 12,
    
    [0] = 22
   orientation:
    i(0()) = 34 >= 22 = 0()
    
    +(0(),y) = y + 33 >= y = y
    
    +(x,0()) = x + 33 >= x = x
    
    i(i(x)) = x + 24 >= x = x
    
    +(i(x),x) = 2x + 23 >= 22 = 0()
    
    +(x,i(x)) = 2x + 23 >= 22 = 0()
    
    i(+(x,y)) = x + y + 23 >= x + y + 35 = +(i(x),i(y))
    
    +(x,+(y,z)) = x + y + z + 22 >= x + y + z + 22 = +(+(x,y),z)
    
    +(+(x,i(y)),y) = x + 2y + 34 >= x = x
    
    +(+(x,y),i(y)) = x + 2y + 34 >= x = x
   problem:
    strict:
     i(+(x,y)) -> +(i(x),i(y))
     +(x,+(y,z)) -> +(+(x,y),z)
    weak:
     i(0()) -> 0()
     +(0(),y) -> y
     +(x,0()) -> x
     i(i(x)) -> x
     +(i(x),x) -> 0()
     +(x,i(x)) -> 0()
     +(+(x,i(y)),y) -> x
     +(+(x,y),i(y)) -> x
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                        [1 8]     [0]
     [+](x0, x1) = x0 + [0 1]x1 + [1],
     
                 
     [i](x0) = x0,
     
           [0]
     [0] = [0]
    orientation:
                     [1 8]    [0]        [1 8]    [0]               
     i(+(x,y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = +(i(x),i(y))
     
                       [1 8]    [1  16]    [8]        [1 8]    [1 8]    [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()
     
                [1 8]    [0]         
     +(0(),y) = [0 1]y + [1] >= y = y
     
                    [0]         
     +(x,0()) = x + [1] >= x = x
     
                         
     i(i(x)) = x >= x = x
     
                 [2 8]    [0]    [0]      
     +(i(x),x) = [0 2]x + [1] >= [0] = 0()
     
                 [2 8]    [0]    [0]      
     +(x,i(x)) = [0 2]x + [1] >= [0] = 0()
     
                          [2  16]    [0]         
     +(+(x,i(y)),y) = x + [0  2 ]y + [2] >= x = x
     
                          [2  16]    [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()
      +(0(),y) -> y
      +(x,0()) -> x
      i(i(x)) -> x
      +(i(x),x) -> 0()
      +(x,i(x)) -> 0()
      +(+(x,i(y)),y) -> x
      +(+(x,y),i(y)) -> x
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                              [1]
      [+](x0, x1) = x0 + x1 + [6],
      
                [1 1]  
      [i](x0) = [0 1]x0,
      
            [1]
      [0] = [2]
     orientation:
                  [1 1]    [1 1]    [7]    [1 1]    [1 1]    [1]               
      i(+(x,y)) = [0 1]x + [0 1]y + [6] >= [0 1]x + [0 1]y + [6] = +(i(x),i(y))
      
                                [2 ]                [2 ]              
      +(x,+(y,z)) = x + y + z + [12] >= x + y + z + [12] = +(+(x,y),z)
      
               [3]    [1]      
      i(0()) = [2] >= [2] = 0()
      
                     [2]         
      +(0(),y) = y + [8] >= y = y
      
                     [2]         
      +(x,0()) = x + [8] >= x = x
      
                [1 2]          
      i(i(x)) = [0 1]x >= x = x
      
                  [2 1]    [1]    [1]      
      +(i(x),x) = [0 2]x + [6] >= [2] = 0()
      
                  [2 1]    [1]    [1]      
      +(x,i(x)) = [0 2]x + [6] >= [2] = 0()
      
                           [2 1]    [2 ]         
      +(+(x,i(y)),y) = x + [0 2]y + [12] >= x = x
      
                           [2 1]    [2 ]         
      +(+(x,y),i(y)) = x + [0 2]y + [12] >= x = x
     problem:
      strict:
       
      weak:
       i(+(x,y)) -> +(i(x),i(y))
       +(x,+(y,z)) -> +(+(x,y),z)
       i(0()) -> 0()
       +(0(),y) -> y
       +(x,0()) -> x
       i(i(x)) -> x
       +(i(x),x) -> 0()
       +(x,i(x)) -> 0()
       +(+(x,i(y)),y) -> x
       +(+(x,y),i(y)) -> x
     Qed