YES
Time: 0.003771
TRS:
 {  f f X -> f g f g f X,
  f g f X -> f g X}
 DP:
  DP:
   {  f# f X -> f# g f X,
      f# f X -> f# g f g f X,
    f# g f X -> f# g X}
  TRS:
  {  f f X -> f g f g f X,
   f g f X -> f g X}
  EDG:
   {(f# g f X -> f# g X, f# g f X -> f# g X)
    (f# f X -> f# g f g f X, f# g f X -> f# g X)
    (f# f X -> f# g f X, f# g f X -> f# g X)}
   STATUS:
    arrows: 0.666667
    SCCS (1):
     Scc:
      {f# g f X -> f# g X}
     
     
     
     SCC (1):
      Strict:
       {f# g f X -> f# g X}
      Weak:
      {  f f X -> f g f g f X,
       f g f X -> f g X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0) = x0 + 1,
        
        [g](x0) = x0,
        
        [f#](x0) = x0
       Strict:
        f# g f X -> f# g X
        1 + 1X >= 0 + 1X
       Weak:
        f g f X -> f g X
        2 + 1X >= 1 + 1X
        f f X -> f g f g f X
        2 + 1X >= 3 + 1X
      Qed