YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
             [1 2]  
   [g](x0) = [0 1]x0,
   
             [0  -&]  
   [a](x0) = [-& -&]x0,
   
               
   [b](x0) = x0,
   
             [0 0]  
   [f](x0) = [0 0]x0
  orientation:
             [0 0]     [0 0]                 
   f(f(X)) = [0 0]X >= [0 0]X = f(a(b(f(X))))
   
                [1 2]             
   f(a(g(X))) = [1 2]X >= X = b(X)
   
               [0  -&]        
   b(X) = X >= [-& -&]X = a(X)
  problem:
   f(f(X)) -> f(a(b(f(X))))
   b(X) -> a(X)
  Arctic Interpretation Processor:
   dimension: 2
   interpretation:
              [0  -&]  
    [a](x0) = [-& -&]x0,
    
              [1  0 ]  
    [b](x0) = [-& 2 ]x0,
    
              [0 0]  
    [f](x0) = [1 1]x0
   orientation:
              [1 1]     [1 1]                 
    f(f(X)) = [2 2]X >= [2 2]X = f(a(b(f(X))))
    
           [1  0 ]     [0  -&]        
    b(X) = [-& 2 ]X >= [-& -&]X = a(X)
   problem:
    f(f(X)) -> f(a(b(f(X))))
   Arctic Interpretation Processor:
    dimension: 2
    interpretation:
               [0  0 ]  
     [a](x0) = [-& -&]x0,
     
               [0  1 ]  
     [b](x0) = [-& 1 ]x0,
     
               [0 3]  
     [f](x0) = [0 2]x0
    orientation:
               [3 5]     [1 3]                 
     f(f(X)) = [2 4]X >= [1 3]X = f(a(b(f(X))))
    problem:
     
    Qed