YES(?,O(n^2))

Problem:
 f(f(X)) -> f(a(b(f(X))))
 f(a(g(X))) -> b(X)
 b(X) -> a(X)

Proof:
 RT Transformation Processor:
  strict:
   f(f(X)) -> f(a(b(f(X))))
   f(a(g(X))) -> b(X)
   b(X) -> a(X)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [g](x0) = x0,
    
    [a](x0) = x0,
    
    [b](x0) = x0 + 31,
    
    [f](x0) = x0 + 1
   orientation:
    f(f(X)) = X + 2 >= X + 33 = f(a(b(f(X))))
    
    f(a(g(X))) = X + 1 >= X + 31 = b(X)
    
    b(X) = X + 31 >= X = a(X)
   problem:
    strict:
     f(f(X)) -> f(a(b(f(X))))
     f(a(g(X))) -> b(X)
    weak:
     b(X) -> a(X)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [g](x0) = x0 + 25,
     
     [a](x0) = x0 + 4,
     
     [b](x0) = x0 + 4,
     
     [f](x0) = x0 + 8
    orientation:
     f(f(X)) = X + 16 >= X + 24 = f(a(b(f(X))))
     
     f(a(g(X))) = X + 37 >= X + 4 = b(X)
     
     b(X) = X + 4 >= X + 4 = a(X)
    problem:
     strict:
      f(f(X)) -> f(a(b(f(X))))
     weak:
      f(a(g(X))) -> b(X)
      b(X) -> a(X)
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                [1  12]     [4]
      [g](x0) = [0  0 ]x0 + [4],
      
                [1 3]     [8]
      [a](x0) = [0 0]x0 + [0],
      
                [1 3]     [9]
      [b](x0) = [0 0]x0 + [1],
      
                [1  10]     [0]
      [f](x0) = [0  0 ]x0 + [3]
     orientation:
                [1  10]    [30]    [1  10]    [29]                
      f(f(X)) = [0  0 ]X + [3 ] >= [0  0 ]X + [3 ] = f(a(b(f(X))))
      
                   [1  12]    [24]    [1 3]    [9]       
      f(a(g(X))) = [0  0 ]X + [3 ] >= [0 0]X + [1] = b(X)
      
             [1 3]    [9]    [1 3]    [8]       
      b(X) = [0 0]X + [1] >= [0 0]X + [0] = a(X)
     problem:
      strict:
       
      weak:
       f(f(X)) -> f(a(b(f(X))))
       f(a(g(X))) -> b(X)
       b(X) -> a(X)
     Qed