YES(?,O(n^1))
TRS:
 {  f f X -> f g f g f X,
  f g f X -> f g X}
 DUP: We consider a non-duplicating system.
  Trs:
   {  f f X -> f g f g f X,
    f g f X -> f g X}
  RLAB:
   Strict:
    {
     f(f) f(f) X -> f(g) g(f) f(g) g(f) f(f) X,
     f(f) f(g) X -> f(g) g(f) f(g) g(f) f(g) X,
     f(g) g(f) f(f) X -> f(g) g(f) X,
     f(g) g(f) f(g) X -> f(g) g(g) X
    }
   Weak:
    {}
   Natural interpretation:
    Strict:
     {
      f(f) f(f) X -> f(g) g(f) f(g) g(f) f(f) X,
      f(f) f(g) X -> f(g) g(f) f(g) g(f) f(g) X,
      f(g) g(f) f(f) X -> f(g) g(f) X,
      f(g) g(f) f(g) X -> f(g) g(g) X
     }
    Weak:
     {}
    Interpretation class: stronglylinear
    [g(1)](X0) = + 1*X0 + 0
    [g(0)](X0) = + 1*X0 + 1
    [f(1)](X0) = + 1*X0 + 0
    [f(0)](X0) = + 1*X0 + 5
    
    Qed