YES(?,O(n^2))

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

Proof:
 RT 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
   interpretation:
    [0] = 29,
    
    [1] = 0,
    
    [*](x0, x1) = x0 + x1,
    
    [i](x0) = x0 + 16
   orientation:
    *(i(x),x) = 2x + 16 >= 0 = 1()
    
    *(1(),y) = y >= y = y
    
    *(x,0()) = x + 29 >= 29 = 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
    interpretation:
     [0] = 1,
     
     [1] = 4,
     
     [*](x0, x1) = x0 + x1 + 4,
     
     [i](x0) = x0
    orientation:
     *(1(),y) = y + 8 >= y = y
     
     *(x,0()) = x + 5 >= 1 = 0()
     
     *(*(x,y),z) = x + y + z + 8 >= x + y + z + 8 = *(x,*(y,z))
     
     *(i(x),x) = 2x + 4 >= 4 = 1()
    problem:
     strict:
      *(*(x,y),z) -> *(x,*(y,z))
     weak:
      *(1(),y) -> y
      *(x,0()) -> 0()
      *(i(x),x) -> 1()
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
            [0]
      [0] = [2],
      
            [0]
      [1] = [6],
      
                    [1 4]          [0]
      [*](x0, x1) = [0 1]x0 + x1 + [4],
      
                [1 0]     [0]
      [i](x0) = [0 0]x0 + [2]
     orientation:
                    [1 8]    [1 4]        [16]    [1 4]    [1 4]        [0]              
      *(*(x,y),z) = [0 1]x + [0 1]y + z + [8 ] >= [0 1]x + [0 1]y + z + [8] = *(x,*(y,z))
      
                     [24]         
      *(1(),y) = y + [10] >= y = y
      
                 [1 4]    [0]    [0]      
      *(x,0()) = [0 1]x + [6] >= [2] = 0()
      
                  [2 0]    [8]    [0]      
      *(i(x),x) = [0 1]x + [6] >= [6] = 1()
     problem:
      strict:
       
      weak:
       *(*(x,y),z) -> *(x,*(y,z))
       *(1(),y) -> y
       *(x,0()) -> 0()
       *(i(x),x) -> 1()
     Qed