YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   f(f(X)) -> f(g(f(g(f(X)))))
   f(g(f(X))) -> f(g(X))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [g](x0) = x0 + 1,
    
    [f](x0) = x0 + 1
   orientation:
    f(f(X)) = X + 2 >= X + 5 = f(g(f(g(f(X)))))
    
    f(g(f(X))) = X + 3 >= X + 2 = f(g(X))
   problem:
    strict:
     f(f(X)) -> f(g(f(g(f(X)))))
    weak:
     f(g(f(X))) -> f(g(X))
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
               [1 1]     [1]
     [g](x0) = [0 0]x0 + [0],
     
               [1 4]     [1]
     [f](x0) = [0 0]x0 + [4]
    orientation:
               [1 4]    [18]    [1 4]    [13]                   
     f(f(X)) = [0 0]X + [4 ] >= [0 0]X + [4 ] = f(g(f(g(f(X)))))
     
                  [1 4]    [7]    [1 1]    [2]          
     f(g(f(X))) = [0 0]X + [4] >= [0 0]X + [4] = f(g(X))
    problem:
     strict:
      
     weak:
      f(f(X)) -> f(g(f(g(f(X)))))
      f(g(f(X))) -> f(g(X))
    Qed