YES

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

Proof:
 DP Processor:
  DPs:
   f#(f(X)) -> b#(f(X))
   f#(f(X)) -> f#(a(b(f(X))))
   f#(a(g(X))) -> b#(X)
  TRS:
   f(f(X)) -> f(a(b(f(X))))
   f(a(g(X))) -> b(X)
   b(X) -> a(X)
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    f(f(X)) -> f(a(b(f(X))))
    f(a(g(X))) -> b(X)
    b(X) -> a(X)
   interpretation:
    [b#](x0) = x0 + 0,
    
    [f#](x0) = 8x0 + 0,
    
    [g](x0) = 11x0,
    
    [a](x0) = -12x0 + 0,
    
    [b](x0) = x0 + 4,
    
    [f](x0) = 2x0 + 8
   orientation:
    f#(f(X)) = 10X + 16 >= 2X + 8 = b#(f(X))
    
    f#(f(X)) = 10X + 16 >= -2X + 8 = f#(a(b(f(X))))
    
    f#(a(g(X))) = 7X + 8 >= X + 0 = b#(X)
    
    f(f(X)) = 4X + 10 >= -8X + 8 = f(a(b(f(X))))
    
    f(a(g(X))) = 1X + 8 >= X + 4 = b(X)
    
    b(X) = X + 4 >= -12X + 0 = a(X)
   problem:
    DPs:
     
    TRS:
     f(f(X)) -> f(a(b(f(X))))
     f(a(g(X))) -> b(X)
     b(X) -> a(X)
   Qed