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