YES
TRS:
 {        f(x, f(x, y)) -> f(f(f(x, a()), a()), a()),
  f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))}
 DP:
  Strict:
   {        f#(x, f(x, y)) -> f#(x, a()),
            f#(x, f(x, y)) -> f#(f(x, a()), a()),
            f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()),
    f#(y, f(x, f(a(), x))) -> f#(x, a()),
    f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)),
    f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())),
    f#(y, f(x, f(a(), x))) -> f#(a(), y)}
  Weak:
  {        f(x, f(x, y)) -> f(f(f(x, a()), a()), a()),
   f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))}
  EDG:
   {(f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()))
    (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(f(x, a()), a()))
    (f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())), f#(x, f(x, y)) -> f#(x, a()))
    (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(x, a()))
    (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(f(x, a()), a()))
    (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()))
    (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(x, a()))
    (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)))
    (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())))
    (f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), y))
    (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(x, a()))
    (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(f(x, a()), a()))
    (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(x, f(x, y)) -> f#(f(f(x, a()), a()), a()))
    (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(x, a()))
    (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)))
    (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(f(a(), x), f(x, a())))
    (f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)), f#(y, f(x, f(a(), x))) -> f#(a(), y))}
   SCCS:
    Scc:
     {f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)),
      f#(y, f(x, f(a(), x))) -> f#(a(), y)}
    SCC:
     Strict:
      {f#(y, f(x, f(a(), x))) -> f#(f(f(a(), x), f(x, a())), f(a(), y)),
       f#(y, f(x, f(a(), x))) -> f#(a(), y)}
     Weak:
     {        f(x, f(x, y)) -> f(f(f(x, a()), a()), a()),
      f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 1
      Automaton:
       {       a_1() -> 11*
               a_0() -> 11*
        f#_1(26, 26) -> 4*
        f#_1(26, 24) -> 4*
        f#_1(26, 23) -> 4*
        f#_1(26, 22) -> 4*
        f#_1(26, 21) -> 4*
        f#_1(26, 19) -> 4*
        f#_1(26, 13) -> 4*
        f#_1(25, 26) -> 4*
        f#_1(25, 24) -> 4*
        f#_1(25, 23) -> 4*
        f#_1(25, 22) -> 4*
        f#_1(25, 21) -> 4*
        f#_1(25, 19) -> 4*
        f#_1(25, 13) -> 4*
        f#_1(24, 26) -> 4*
        f#_1(24, 24) -> 4*
        f#_1(24, 23) -> 4*
        f#_1(24, 22) -> 4*
        f#_1(24, 21) -> 4*
        f#_1(24, 19) -> 4*
        f#_1(24, 13) -> 4*
        f#_1(23, 26) -> 4*
        f#_1(23, 24) -> 4*
        f#_1(23, 23) -> 4*
        f#_1(23, 22) -> 4*
        f#_1(23, 21) -> 4*
        f#_1(23, 19) -> 4*
        f#_1(23, 13) -> 4*
        f#_1(21, 26) -> 4*
        f#_1(21, 24) -> 4*
        f#_1(21, 23) -> 4*
        f#_1(21, 22) -> 4*
        f#_1(21, 21) -> 4*
        f#_1(21, 19) -> 4*
        f#_1(21, 13) -> 4*
        f#_1(20, 26) -> 4*
        f#_1(20, 24) -> 4*
        f#_1(20, 23) -> 4*
        f#_1(20, 22) -> 4*
        f#_1(20, 21) -> 4*
        f#_1(20, 19) -> 4*
        f#_1(20, 13) -> 4*
        f#_1(18, 26) -> 4*
        f#_1(18, 24) -> 4*
        f#_1(18, 23) -> 4*
        f#_1(18, 22) -> 4*
        f#_1(18, 21) -> 4*
        f#_1(18, 19) -> 4*
        f#_1(18, 13) -> 4*
        f#_1(15, 26) -> 4*
        f#_1(15, 24) -> 4*
        f#_1(15, 23) -> 4*
        f#_1(15, 22) -> 4*
        f#_1(15, 21) -> 4*
        f#_1(15, 19) -> 4*
        f#_1(15, 13) -> 4*
        f#_1(11, 26) -> 4*
        f#_1(11, 25) -> 4*
        f#_1(11, 24) -> 4*
        f#_1(11, 23) -> 4*
        f#_1(11, 21) -> 4*
        f#_1(11, 20) -> 4*
        f#_1(11, 18) -> 4*
        f#_1(11, 15) -> 4*
        f#_0(26, 26) -> 4*
        f#_0(26, 24) -> 4*
        f#_0(26, 23) -> 4*
        f#_0(26, 22) -> 4*
        f#_0(26, 21) -> 4*
        f#_0(26, 19) -> 4*
        f#_0(26, 16) -> 4*
        f#_0(26, 13) -> 4*
        f#_0(25, 26) -> 4*
        f#_0(25, 24) -> 4*
        f#_0(25, 23) -> 4*
        f#_0(25, 22) -> 4*
        f#_0(25, 21) -> 4*
        f#_0(25, 19) -> 4*
        f#_0(25, 16) -> 4*
        f#_0(25, 13) -> 4*
        f#_0(24, 26) -> 4*
        f#_0(24, 24) -> 4*
        f#_0(24, 23) -> 4*
        f#_0(24, 22) -> 4*
        f#_0(24, 21) -> 4*
        f#_0(24, 19) -> 4*
        f#_0(24, 16) -> 4*
        f#_0(24, 13) -> 4*
        f#_0(23, 26) -> 4*
        f#_0(23, 24) -> 4*
        f#_0(23, 23) -> 4*
        f#_0(23, 22) -> 4*
        f#_0(23, 21) -> 4*
        f#_0(23, 19) -> 4*
        f#_0(23, 16) -> 4*
        f#_0(23, 13) -> 4*
        f#_0(21, 26) -> 4*
        f#_0(21, 24) -> 4*
        f#_0(21, 23) -> 4*
        f#_0(21, 22) -> 4*
        f#_0(21, 21) -> 4*
        f#_0(21, 19) -> 4*
        f#_0(21, 16) -> 4*
        f#_0(21, 13) -> 4*
        f#_0(20, 26) -> 4*
        f#_0(20, 24) -> 4*
        f#_0(20, 23) -> 4*
        f#_0(20, 22) -> 4*
        f#_0(20, 21) -> 4*
        f#_0(20, 19) -> 4*
        f#_0(20, 16) -> 4*
        f#_0(20, 13) -> 4*
        f#_0(18, 26) -> 4*
        f#_0(18, 24) -> 4*
        f#_0(18, 23) -> 4*
        f#_0(18, 22) -> 4*
        f#_0(18, 21) -> 4*
        f#_0(18, 19) -> 4*
        f#_0(18, 16) -> 4*
        f#_0(18, 13) -> 4*
        f#_0(15, 26) -> 4*
        f#_0(15, 24) -> 4*
        f#_0(15, 23) -> 4*
        f#_0(15, 22) -> 4*
        f#_0(15, 21) -> 4*
        f#_0(15, 19) -> 4*
        f#_0(15, 16) -> 4*
        f#_0(15, 13) -> 4*
        f#_0(11, 26) -> 4*
        f#_0(11, 25) -> 4*
        f#_0(11, 24) -> 4*
        f#_0(11, 23) -> 4*
        f#_0(11, 21) -> 4*
        f#_0(11, 20) -> 4*
        f#_0(11, 18) -> 4*
        f#_0(11, 15) -> 4*
         f_1(16, 16) -> 15*
         f_1(11, 26) -> 13*
         f_1(11, 25) -> 13*
         f_1(11, 24) -> 13*
         f_1(11, 23) -> 13*
         f_1(11, 21) -> 13*
         f_1(11, 20) -> 13*
         f_1(11, 18) -> 13*
         f_1(11, 15) -> 13*
         f_1(11, 11) -> 16*
         f_0(26, 26) -> 18* | 15 | 10
         f_0(26, 25) -> 18* | 15 | 10
         f_0(26, 24) -> 10*
         f_0(26, 23) -> 10*
         f_0(26, 22) -> 10*
         f_0(26, 21) -> 18* | 15 | 10
         f_0(26, 20) -> 18* | 15 | 10
         f_0(26, 19) -> 18* | 15 | 10
         f_0(26, 18) -> 10*
         f_0(26, 17) -> 18* | 15 | 10
         f_0(26, 16) -> 24* | 22 | 18 | 15 | 13 | 10
         f_0(26, 15) -> 10*
         f_0(26, 13) -> 10*
         f_0(26, 12) -> 18* | 15 | 10
         f_0(26, 11) -> 26* | 25 | 21 | 20 | 19 | 18 | 17 | 15 | 13 | 12 | 10
         f_0(26, 10) -> 10*
         f_0(25, 26) -> 10*
         f_0(25, 25) -> 10*
         f_0(25, 24) -> 10*
         f_0(25, 23) -> 10*
         f_0(25, 22) -> 10*
         f_0(25, 21) -> 10*
         f_0(25, 20) -> 10*
         f_0(25, 19) -> 10*
         f_0(25, 18) -> 10*
         f_0(25, 17) -> 10*
         f_0(25, 16) -> 22* | 13 | 10
         f_0(25, 15) -> 10*
         f_0(25, 13) -> 10*
         f_0(25, 12) -> 10*
         f_0(25, 11) -> 26* | 25 | 21 | 20 | 19 | 18 | 17 | 15 | 13 | 12 | 10
         f_0(25, 10) -> 10*
         f_0(24, 26) -> 18* | 15 | 10
         f_0(24, 25) -> 18* | 15 | 10
         f_0(24, 24) -> 10*
         f_0(24, 23) -> 10*
         f_0(24, 22) -> 10*
         f_0(24, 21) -> 18* | 15 | 10
         f_0(24, 20) -> 18* | 15 | 10
         f_0(24, 19) -> 18* | 15 | 10
         f_0(24, 18) -> 10*
         f_0(24, 17) -> 18* | 15 | 10
         f_0(24, 16) -> 23* | 22 | 15 | 13 | 10
         f_0(24, 15) -> 10*
         f_0(24, 13) -> 10*
         f_0(24, 12) -> 18* | 15 | 10
         f_0(24, 11) -> 25* | 20 | 18 | 15 | 12
         f_0(24, 10) -> 10*
         f_0(23, 26) -> 18* | 15 | 10
         f_0(23, 25) -> 18* | 15 | 10
         f_0(23, 24) -> 10*
         f_0(23, 23) -> 10*
         f_0(23, 22) -> 10*
         f_0(23, 21) -> 18* | 15 | 10
         f_0(23, 20) -> 18* | 15 | 10
         f_0(23, 19) -> 18* | 15 | 10
         f_0(23, 18) -> 10*
         f_0(23, 17) -> 18* | 15 | 10
         f_0(23, 16) -> 23* | 22 | 15 | 13 | 10
         f_0(23, 15) -> 10*
         f_0(23, 13) -> 10*
         f_0(23, 12) -> 18* | 15 | 10
         f_0(23, 11) -> 25* | 20 | 18 | 15 | 12
         f_0(23, 10) -> 10*
         f_0(22, 26) -> 18* | 15 | 10
         f_0(22, 25) -> 18* | 15 | 10
         f_0(22, 24) -> 10*
         f_0(22, 23) -> 10*
         f_0(22, 22) -> 10*
         f_0(22, 21) -> 18* | 15 | 10
         f_0(22, 20) -> 18* | 15 | 10
         f_0(22, 19) -> 18* | 15 | 10
         f_0(22, 18) -> 10*
         f_0(22, 17) -> 18* | 15 | 10
         f_0(22, 16) -> 23* | 22 | 15 | 13 | 10
         f_0(22, 15) -> 10*
         f_0(22, 13) -> 10*
         f_0(22, 12) -> 18* | 15 | 10
         f_0(22, 11) -> 25* | 20 | 18 | 15 | 12
         f_0(22, 10) -> 10*
         f_0(21, 26) -> 18* | 15 | 10
         f_0(21, 25) -> 18* | 15 | 10
         f_0(21, 24) -> 10*
         f_0(21, 23) -> 10*
         f_0(21, 22) -> 10*
         f_0(21, 21) -> 18* | 15 | 10
         f_0(21, 20) -> 18* | 15 | 10
         f_0(21, 19) -> 18* | 15 | 10
         f_0(21, 18) -> 10*
         f_0(21, 17) -> 18* | 15 | 10
         f_0(21, 16) -> 24* | 22 | 18 | 15 | 13 | 10
         f_0(21, 15) -> 10*
         f_0(21, 13) -> 10*
         f_0(21, 12) -> 18* | 15 | 10
         f_0(21, 11) -> 26* | 25 | 21 | 20 | 19 | 18 | 17 | 15 | 13 | 12 | 10
         f_0(21, 10) -> 10*
         f_0(20, 26) -> 10*
         f_0(20, 25) -> 10*
         f_0(20, 24) -> 10*
         f_0(20, 23) -> 10*
         f_0(20, 22) -> 10*
         f_0(20, 21) -> 10*
         f_0(20, 20) -> 10*
         f_0(20, 19) -> 10*
         f_0(20, 18) -> 10*
         f_0(20, 17) -> 10*
         f_0(20, 16) -> 22* | 13 | 10
         f_0(20, 15) -> 10*
         f_0(20, 13) -> 10*
         f_0(20, 12) -> 10*
         f_0(20, 11) -> 19* | 17 | 13 | 12 | 10
         f_0(20, 10) -> 10*
         f_0(19, 26) -> 18* | 15 | 10
         f_0(19, 25) -> 18* | 15 | 10
         f_0(19, 24) -> 10*
         f_0(19, 23) -> 10*
         f_0(19, 22) -> 10*
         f_0(19, 21) -> 18* | 15 | 10
         f_0(19, 20) -> 18* | 15 | 10
         f_0(19, 19) -> 18* | 15 | 10
         f_0(19, 18) -> 10*
         f_0(19, 17) -> 18* | 15 | 10
         f_0(19, 16) -> 24* | 22 | 18 | 15 | 13 | 10
         f_0(19, 15) -> 10*
         f_0(19, 13) -> 10*
         f_0(19, 12) -> 18* | 15 | 10
         f_0(19, 11) -> 26* | 25 | 21 | 20 | 19 | 18 | 17 | 15 | 13 | 12 | 10
         f_0(19, 10) -> 10*
         f_0(18, 26) -> 10*
         f_0(18, 25) -> 10*
         f_0(18, 24) -> 10*
         f_0(18, 23) -> 10*
         f_0(18, 22) -> 10*
         f_0(18, 21) -> 10*
         f_0(18, 20) -> 10*
         f_0(18, 19) -> 10*
         f_0(18, 18) -> 10*
         f_0(18, 17) -> 10*
         f_0(18, 16) -> 22* | 13 | 10
         f_0(18, 15) -> 10*
         f_0(18, 13) -> 10*
         f_0(18, 12) -> 10*
         f_0(18, 11) -> 25* | 20 | 18 | 15 | 12
         f_0(18, 10) -> 10*
         f_0(17, 26) -> 10*
         f_0(17, 25) -> 10*
         f_0(17, 24) -> 10*
         f_0(17, 23) -> 10*
         f_0(17, 22) -> 10*
         f_0(17, 21) -> 10*
         f_0(17, 20) -> 10*
         f_0(17, 19) -> 10*
         f_0(17, 18) -> 10*
         f_0(17, 17) -> 10*
         f_0(17, 16) -> 10*
         f_0(17, 15) -> 10*
         f_0(17, 13) -> 10*
         f_0(17, 12) -> 10*
         f_0(17, 11) -> 19* | 17 | 13 | 12 | 10
         f_0(17, 10) -> 10*
         f_0(16, 26) -> 18* | 15 | 10
         f_0(16, 25) -> 18* | 15 | 10
         f_0(16, 24) -> 10*
         f_0(16, 23) -> 10*
         f_0(16, 22) -> 10*
         f_0(16, 21) -> 18* | 15 | 10
         f_0(16, 20) -> 18* | 15 | 10
         f_0(16, 19) -> 18* | 15 | 10
         f_0(16, 18) -> 10*
         f_0(16, 17) -> 18* | 15 | 10
         f_0(16, 16) -> 15*
         f_0(16, 15) -> 10*
         f_0(16, 13) -> 10*
         f_0(16, 12) -> 15*
         f_0(16, 11) -> 12*
         f_0(16, 10) -> 10*
         f_0(15, 26) -> 10*
         f_0(15, 25) -> 10*
         f_0(15, 24) -> 10*
         f_0(15, 23) -> 10*
         f_0(15, 22) -> 10*
         f_0(15, 21) -> 10*
         f_0(15, 20) -> 10*
         f_0(15, 19) -> 10*
         f_0(15, 18) -> 10*
         f_0(15, 17) -> 10*
         f_0(15, 16) -> 22* | 13 | 10
         f_0(15, 15) -> 10*
         f_0(15, 13) -> 10*
         f_0(15, 12) -> 10*
         f_0(15, 11) -> 12*
         f_0(15, 10) -> 10*
         f_0(13, 26) -> 18* | 15 | 10
         f_0(13, 25) -> 18* | 15 | 10
         f_0(13, 24) -> 10*
         f_0(13, 23) -> 10*
         f_0(13, 22) -> 10*
         f_0(13, 21) -> 18* | 15 | 10
         f_0(13, 20) -> 18* | 15 | 10
         f_0(13, 19) -> 18* | 15 | 10
         f_0(13, 18) -> 10*
         f_0(13, 17) -> 18* | 15 | 10
         f_0(13, 16) -> 15*
         f_0(13, 15) -> 10*
         f_0(13, 13) -> 10*
         f_0(13, 12) -> 15*
         f_0(13, 11) -> 12*
         f_0(13, 10) -> 10*
         f_0(12, 26) -> 10*
         f_0(12, 25) -> 10*
         f_0(12, 24) -> 10*
         f_0(12, 23) -> 10*
         f_0(12, 22) -> 10*
         f_0(12, 21) -> 10*
         f_0(12, 20) -> 10*
         f_0(12, 19) -> 10*
         f_0(12, 18) -> 10*
         f_0(12, 17) -> 10*
         f_0(12, 16) -> 10*
         f_0(12, 15) -> 10*
         f_0(12, 13) -> 10*
         f_0(12, 12) -> 10*
         f_0(12, 11) -> 19* | 17 | 13 | 12 | 10
         f_0(12, 10) -> 10*
         f_0(11, 26) -> 13*
         f_0(11, 25) -> 13*
         f_0(11, 24) -> 13*
         f_0(11, 23) -> 13*
         f_0(11, 22) -> 13*
         f_0(11, 21) -> 13*
         f_0(11, 20) -> 13*
         f_0(11, 19) -> 13*
         f_0(11, 18) -> 13*
         f_0(11, 17) -> 13*
         f_0(11, 16) -> 13*
         f_0(11, 15) -> 13*
         f_0(11, 13) -> 13*
         f_0(11, 12) -> 13*
         f_0(11, 11) -> 16*
         f_0(11, 10) -> 13*
         f_0(10, 26) -> 10*
         f_0(10, 25) -> 10*
         f_0(10, 24) -> 10*
         f_0(10, 23) -> 10*
         f_0(10, 22) -> 10*
         f_0(10, 21) -> 10*
         f_0(10, 20) -> 10*
         f_0(10, 19) -> 10*
         f_0(10, 18) -> 10*
         f_0(10, 17) -> 10*
         f_0(10, 16) -> 22* | 13 | 10
         f_0(10, 15) -> 10*
         f_0(10, 13) -> 10*
         f_0(10, 12) -> 10*
         f_0(10, 11) -> 25* | 20 | 18 | 15 | 12
         f_0(10, 10) -> 10*}
      Strict:
       {f#(y, f(x, f(a(), x))) -> f#(a(), y)}
      EDG:
       {(f#(y, f(x, f(a(), x))) -> f#(a(), y), f#(y, f(x, f(a(), x))) -> f#(a(), y))}
       SCCS:
        Scc:
         {f#(y, f(x, f(a(), x))) -> f#(a(), y)}
        SCC:
         Strict:
          {f#(y, f(x, f(a(), x))) -> f#(a(), y)}
         Weak:
         {        f(x, f(x, y)) -> f(f(f(x, a()), a()), a()),
          f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))}
         POLY:
          Argument Filtering:
           pi(a) = [], pi(f#) = [0,1], pi(f) = []
          Usable Rules:
           {}
          Interpretation:
           [f#](x0, x1) = x0 + x1,
           [f] = 1,
           [a] = 0
          Strict:
           {}
          Weak:
           {        f(x, f(x, y)) -> f(f(f(x, a()), a()), a()),
            f(y, f(x, f(a(), x))) -> f(f(f(a(), x), f(x, a())), f(a(), y))}
          Qed