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