YES
Time: 0.006826
TRS:
 {f(f(x, a()), y) -> f(y, f(x, y))}
 DP:
  DP:
   {f#(f(x, a()), y) -> f#(y, f(x, y)),
    f#(f(x, a()), y) -> f#(x, y)}
  TRS:
  {f(f(x, a()), y) -> f(y, f(x, y))}
  EDG:
   {(f#(f(x, a()), y) -> f#(x, y), f#(f(x, a()), y) -> f#(x, y))
    (f#(f(x, a()), y) -> f#(x, y), f#(f(x, a()), y) -> f#(y, f(x, y)))
    (f#(f(x, a()), y) -> f#(y, f(x, y)), f#(f(x, a()), y) -> f#(y, f(x, y)))
    (f#(f(x, a()), y) -> f#(y, f(x, y)), f#(f(x, a()), y) -> f#(x, y))}
   SCCS (1):
    Scc:
     {f#(f(x, a()), y) -> f#(y, f(x, y)),
      f#(f(x, a()), y) -> f#(x, y)}
    SCC (2):
     Strict:
      {f#(f(x, a()), y) -> f#(y, f(x, y)),
       f#(f(x, a()), y) -> f#(x, y)}
     Weak:
     {f(f(x, a()), y) -> f(y, f(x, y))}
     BOUND:
      Bound: top(-raise)-DP-bounded by 2
      Automaton:
       {      a_0() -> 7*
        f#_2(9, 10) -> 4*
         f#_1(8, 9) -> 4*
         f#_1(7, 9) -> 4*
         f#_0(8, 8) -> 4*
         f#_0(7, 8) -> 4*
         f_2(9, 10) -> 10*
          f_2(8, 9) -> 10*
          f_2(7, 9) -> 10*
         f_1(9, 10) -> 9*
          f_1(8, 9) -> 9*
          f_1(8, 8) -> 9*
          f_1(7, 8) -> 9*
          f_0(8, 8) -> 8*
          f_0(8, 7) -> 8*
          f_0(7, 8) -> 8*
          f_0(7, 7) -> 8*}
      Strict:
       {f#(f(x, a()), y) -> f#(x, y)}
      EDG:
       {(f#(f(x, a()), y) -> f#(x, y), f#(f(x, a()), y) -> f#(x, y))}
       SCCS (1):
        Scc:
         {f#(f(x, a()), y) -> f#(x, y)}
        SCC (1):
         Strict:
          {f#(f(x, a()), y) -> f#(x, y)}
         Weak:
         {f(f(x, a()), y) -> f(y, f(x, y))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed