YES(?,O(n^2))

Problem:
 div(X,e()) -> i(X)
 i(div(X,Y)) -> div(Y,X)
 div(div(X,Y),Z) -> div(Y,div(i(X),Z))

Proof:
 RT Transformation Processor:
  strict:
   div(X,e()) -> i(X)
   i(div(X,Y)) -> div(Y,X)
   div(div(X,Y),Z) -> div(Y,div(i(X),Z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [i](x0) = x0 + 2,
    
    [div](x0, x1) = x0 + x1 + 6,
    
    [e] = 0
   orientation:
    div(X,e()) = X + 6 >= X + 2 = i(X)
    
    i(div(X,Y)) = X + Y + 8 >= X + Y + 6 = div(Y,X)
    
    div(div(X,Y),Z) = X + Y + Z + 12 >= X + Y + Z + 14 = div(Y,div(i(X),Z))
   problem:
    strict:
     div(div(X,Y),Z) -> div(Y,div(i(X),Z))
    weak:
     div(X,e()) -> i(X)
     i(div(X,Y)) -> div(Y,X)
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
               [1 8]     [10]
     [i](x0) = [0 1]x0 + [0 ],
     
                     [1 8]          [0]
     [div](x0, x1) = [0 1]x0 + x1 + [2],
     
           [15]
     [e] = [0 ]
    orientation:
                       [1  16]    [1 8]        [16]    [1  16]    [1 8]        [10]                     
     div(div(X,Y),Z) = [0  1 ]X + [0 1]Y + Z + [4 ] >= [0  1 ]X + [0 1]Y + Z + [4 ] = div(Y,div(i(X),Z))
     
                  [1 8]    [15]    [1 8]    [10]       
     div(X,e()) = [0 1]X + [2 ] >= [0 1]X + [0 ] = i(X)
     
                   [1  16]    [1 8]    [26]        [1 8]    [0]           
     i(div(X,Y)) = [0  1 ]X + [0 1]Y + [2 ] >= X + [0 1]Y + [2] = div(Y,X)
    problem:
     strict:
      
     weak:
      div(div(X,Y),Z) -> div(Y,div(i(X),Z))
      div(X,e()) -> i(X)
      i(div(X,Y)) -> div(Y,X)
    Qed