YES(?,O(n^2))

Problem:
 g(f(x,y),z) -> f(x,g(y,z))
 g(h(x,y),z) -> g(x,f(y,z))
 g(x,h(y,z)) -> h(g(x,y),z)

Proof:
 RT Transformation Processor:
  strict:
   g(f(x,y),z) -> f(x,g(y,z))
   g(h(x,y),z) -> g(x,f(y,z))
   g(x,h(y,z)) -> h(g(x,y),z)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [h](x0, x1) = x0 + x1 + 1,
    
    [g](x0, x1) = x0 + x1,
    
    [f](x0, x1) = x0 + x1
   orientation:
    g(f(x,y),z) = x + y + z >= x + y + z = f(x,g(y,z))
    
    g(h(x,y),z) = x + y + z + 1 >= x + y + z = g(x,f(y,z))
    
    g(x,h(y,z)) = x + y + z + 1 >= x + y + z + 1 = h(g(x,y),z)
   problem:
    strict:
     g(f(x,y),z) -> f(x,g(y,z))
     g(x,h(y,z)) -> h(g(x,y),z)
    weak:
     g(h(x,y),z) -> g(x,f(y,z))
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                        [1 2]     [2]
     [h](x0, x1) = x0 + [0 0]x1 + [9],
     
                   [1 2]     [1 2]     [2 ]
     [g](x0, x1) = [0 1]x0 + [0 1]x1 + [10],
     
                   [1 0]          [3]
     [f](x0, x1) = [0 0]x0 + x1 + [6]
    orientation:
                   [1 0]    [1 2]    [1 2]    [17]    [1 0]    [1 2]    [1 2]    [5 ]              
     g(f(x,y),z) = [0 0]x + [0 1]y + [0 1]z + [16] >= [0 0]x + [0 1]y + [0 1]z + [16] = f(x,g(y,z))
     
                   [1 2]    [1 2]    [1 2]    [22]    [1 2]    [1 2]    [1 2]    [4 ]              
     g(x,h(y,z)) = [0 1]x + [0 1]y + [0 0]z + [19] >= [0 1]x + [0 1]y + [0 0]z + [19] = h(g(x,y),z)
     
                   [1 2]    [1 2]    [1 2]    [22]    [1 2]    [1 0]    [1 2]    [17]              
     g(h(x,y),z) = [0 1]x + [0 0]y + [0 1]z + [19] >= [0 1]x + [0 0]y + [0 1]z + [16] = g(x,f(y,z))
    problem:
     strict:
      
     weak:
      g(f(x,y),z) -> f(x,g(y,z))
      g(x,h(y,z)) -> h(g(x,y),z)
      g(h(x,y),z) -> g(x,f(y,z))
    Qed