YES(?,O(n^2))

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

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