YES(?,O(n^2))

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

Proof:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [g](x0) = x0,
     
     [a](x0) = x0,
     
     [b](x0) = x0 + 1,
     
     [f](x0) = x0
    orientation:
     f(f(X)) = X >= X + 1 = f(a(b(f(X))))
     
     f(a(g(X))) = X >= X + 1 = b(X)
     
     b(X) = X + 1 >= 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
     max_matrix:
      1
      interpretation:
       [g](x0) = x0 + 1,
       
       [a](x0) = x0 + 1,
       
       [b](x0) = x0 + 1,
       
       [f](x0) = x0
      orientation:
       f(f(X)) = X >= X + 2 = f(a(b(f(X))))
       
       f(a(g(X))) = X + 2 >= X + 1 = b(X)
       
       b(X) = X + 1 >= X + 1 = 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
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                   [1 0]  
         [g](x0) = [0 0]x0,
         
                   [1 0]  
         [a](x0) = [0 0]x0,
         
                   [1 0]  
         [b](x0) = [0 0]x0,
         
                   [1 1]     [0]
         [f](x0) = [0 1]x0 + [1]
        orientation:
                   [1 2]    [1]    [1 1]    [0]                
         f(f(X)) = [0 1]X + [2] >= [0 0]X + [1] = f(a(b(f(X))))
         
                      [1 0]    [0]    [1 0]        
         f(a(g(X))) = [0 0]X + [1] >= [0 0]X = b(X)
         
                [1 0]     [1 0]        
         b(X) = [0 0]X >= [0 0]X = a(X)
        problem:
         strict:
          
         weak:
          f(f(X)) -> f(a(b(f(X))))
          f(a(g(X))) -> b(X)
          b(X) -> a(X)
        Qed