YES
Time: 22.977839
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:
  DP:
   {        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)}
  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))}
  EDG:
   {(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#(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#(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#(x, 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#(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#(x, 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#(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#(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#(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 (1):
    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 (2):
     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() -> 9*
               a_0() -> 9*
        f#_1(25, 25) -> 4*
        f#_1(25, 23) -> 4*
        f#_1(25, 22) -> 4*
        f#_1(25, 21) -> 4*
        f#_1(25, 19) -> 4*
        f#_1(25, 17) -> 4*
        f#_1(25, 14) -> 4*
        f#_1(24, 25) -> 4*
        f#_1(24, 23) -> 4*
        f#_1(24, 22) -> 4*
        f#_1(24, 21) -> 4*
        f#_1(24, 19) -> 4*
        f#_1(24, 17) -> 4*
        f#_1(24, 14) -> 4*
        f#_1(23, 25) -> 4*
        f#_1(23, 23) -> 4*
        f#_1(23, 22) -> 4*
        f#_1(23, 21) -> 4*
        f#_1(23, 19) -> 4*
        f#_1(23, 17) -> 4*
        f#_1(23, 14) -> 4*
        f#_1(21, 25) -> 4*
        f#_1(21, 23) -> 4*
        f#_1(21, 22) -> 4*
        f#_1(21, 21) -> 4*
        f#_1(21, 19) -> 4*
        f#_1(21, 17) -> 4*
        f#_1(21, 14) -> 4*
        f#_1(20, 25) -> 4*
        f#_1(20, 23) -> 4*
        f#_1(20, 22) -> 4*
        f#_1(20, 21) -> 4*
        f#_1(20, 19) -> 4*
        f#_1(20, 17) -> 4*
        f#_1(20, 14) -> 4*
        f#_1(18, 25) -> 4*
        f#_1(18, 23) -> 4*
        f#_1(18, 22) -> 4*
        f#_1(18, 21) -> 4*
        f#_1(18, 19) -> 4*
        f#_1(18, 17) -> 4*
        f#_1(18, 14) -> 4*
        f#_1(16, 25) -> 4*
        f#_1(16, 23) -> 4*
        f#_1(16, 22) -> 4*
        f#_1(16, 21) -> 4*
        f#_1(16, 19) -> 4*
        f#_1(16, 17) -> 4*
        f#_1(16, 14) -> 4*
         f#_1(9, 25) -> 4*
         f#_1(9, 24) -> 4*
         f#_1(9, 23) -> 4*
         f#_1(9, 21) -> 4*
         f#_1(9, 20) -> 4*
         f#_1(9, 18) -> 4*
         f#_1(9, 16) -> 4*
        f#_0(25, 25) -> 4*
        f#_0(25, 23) -> 4*
        f#_0(25, 22) -> 4*
        f#_0(25, 21) -> 4*
        f#_0(25, 19) -> 4*
        f#_0(25, 17) -> 4*
        f#_0(25, 15) -> 4*
        f#_0(25, 14) -> 4*
        f#_0(24, 25) -> 4*
        f#_0(24, 23) -> 4*
        f#_0(24, 22) -> 4*
        f#_0(24, 21) -> 4*
        f#_0(24, 19) -> 4*
        f#_0(24, 17) -> 4*
        f#_0(24, 15) -> 4*
        f#_0(24, 14) -> 4*
        f#_0(23, 25) -> 4*
        f#_0(23, 23) -> 4*
        f#_0(23, 22) -> 4*
        f#_0(23, 21) -> 4*
        f#_0(23, 19) -> 4*
        f#_0(23, 17) -> 4*
        f#_0(23, 15) -> 4*
        f#_0(23, 14) -> 4*
        f#_0(21, 25) -> 4*
        f#_0(21, 23) -> 4*
        f#_0(21, 22) -> 4*
        f#_0(21, 21) -> 4*
        f#_0(21, 19) -> 4*
        f#_0(21, 17) -> 4*
        f#_0(21, 15) -> 4*
        f#_0(21, 14) -> 4*
        f#_0(20, 25) -> 4*
        f#_0(20, 23) -> 4*
        f#_0(20, 22) -> 4*
        f#_0(20, 21) -> 4*
        f#_0(20, 19) -> 4*
        f#_0(20, 17) -> 4*
        f#_0(20, 15) -> 4*
        f#_0(20, 14) -> 4*
        f#_0(18, 25) -> 4*
        f#_0(18, 23) -> 4*
        f#_0(18, 22) -> 4*
        f#_0(18, 21) -> 4*
        f#_0(18, 19) -> 4*
        f#_0(18, 17) -> 4*
        f#_0(18, 15) -> 4*
        f#_0(18, 14) -> 4*
        f#_0(16, 25) -> 4*
        f#_0(16, 23) -> 4*
        f#_0(16, 22) -> 4*
        f#_0(16, 21) -> 4*
        f#_0(16, 19) -> 4*
        f#_0(16, 17) -> 4*
        f#_0(16, 15) -> 4*
        f#_0(16, 14) -> 4*
         f#_0(9, 25) -> 4*
         f#_0(9, 24) -> 4*
         f#_0(9, 23) -> 4*
         f#_0(9, 21) -> 4*
         f#_0(9, 20) -> 4*
         f#_0(9, 18) -> 4*
         f#_0(9, 16) -> 4*
         f_1(15, 15) -> 16*
          f_1(9, 25) -> 14*
          f_1(9, 24) -> 14*
          f_1(9, 23) -> 14*
          f_1(9, 21) -> 14*
          f_1(9, 20) -> 14*
          f_1(9, 18) -> 14*
          f_1(9, 16) -> 14*
           f_1(9, 9) -> 15*
         f_0(25, 25) -> 18* | 16 | 10
         f_0(25, 24) -> 18* | 16 | 10
         f_0(25, 23) -> 10*
         f_0(25, 22) -> 10*
         f_0(25, 21) -> 18* | 16 | 10
         f_0(25, 20) -> 18* | 16 | 10
         f_0(25, 19) -> 18* | 16 | 10
         f_0(25, 18) -> 10*
         f_0(25, 17) -> 18* | 16 | 10
         f_0(25, 16) -> 10*
         f_0(25, 15) -> 23* | 22 | 18 | 16 | 14 | 10
         f_0(25, 14) -> 10*
         f_0(25, 12) -> 18* | 16 | 10
         f_0(25, 10) -> 10*
          f_0(25, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 10
         f_0(24, 25) -> 10*
         f_0(24, 24) -> 10*
         f_0(24, 23) -> 10*
         f_0(24, 22) -> 10*
         f_0(24, 21) -> 10*
         f_0(24, 20) -> 10*
         f_0(24, 19) -> 10*
         f_0(24, 18) -> 10*
         f_0(24, 17) -> 10*
         f_0(24, 16) -> 10*
         f_0(24, 15) -> 22* | 14 | 10
         f_0(24, 14) -> 10*
         f_0(24, 12) -> 10*
         f_0(24, 10) -> 10*
          f_0(24, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 10
         f_0(23, 25) -> 18* | 16 | 10
         f_0(23, 24) -> 18* | 16 | 10
         f_0(23, 23) -> 10*
         f_0(23, 22) -> 10*
         f_0(23, 21) -> 18* | 16 | 10
         f_0(23, 20) -> 18* | 16 | 10
         f_0(23, 19) -> 18* | 16 | 10
         f_0(23, 18) -> 10*
         f_0(23, 17) -> 18* | 16 | 10
         f_0(23, 16) -> 10*
         f_0(23, 15) -> 23* | 22 | 18 | 16 | 14 | 10
         f_0(23, 14) -> 10*
         f_0(23, 12) -> 18* | 16 | 10
         f_0(23, 10) -> 10*
          f_0(23, 9) -> 24* | 20 | 18 | 16 | 12
         f_0(22, 25) -> 18* | 16 | 10
         f_0(22, 24) -> 18* | 16 | 10
         f_0(22, 23) -> 10*
         f_0(22, 22) -> 10*
         f_0(22, 21) -> 18* | 16 | 10
         f_0(22, 20) -> 18* | 16 | 10
         f_0(22, 19) -> 18* | 16 | 10
         f_0(22, 18) -> 10*
         f_0(22, 17) -> 18* | 16 | 10
         f_0(22, 16) -> 10*
         f_0(22, 15) -> 18* | 16 | 10
         f_0(22, 14) -> 10*
         f_0(22, 12) -> 18* | 16 | 10
         f_0(22, 10) -> 10*
          f_0(22, 9) -> 24* | 20 | 18 | 16 | 12
         f_0(21, 25) -> 18* | 16 | 10
         f_0(21, 24) -> 18* | 16 | 10
         f_0(21, 23) -> 10*
         f_0(21, 22) -> 10*
         f_0(21, 21) -> 18* | 16 | 10
         f_0(21, 20) -> 18* | 16 | 10
         f_0(21, 19) -> 18* | 16 | 10
         f_0(21, 18) -> 10*
         f_0(21, 17) -> 18* | 16 | 10
         f_0(21, 16) -> 10*
         f_0(21, 15) -> 23* | 22 | 18 | 16 | 14 | 10
         f_0(21, 14) -> 10*
         f_0(21, 12) -> 18* | 16 | 10
         f_0(21, 10) -> 10*
          f_0(21, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 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) -> 10*
         f_0(20, 15) -> 22* | 14 | 10
         f_0(20, 14) -> 10*
         f_0(20, 12) -> 10*
         f_0(20, 10) -> 10*
          f_0(20, 9) -> 19* | 17 | 14 | 12 | 10
         f_0(19, 25) -> 18* | 16 | 10
         f_0(19, 24) -> 18* | 16 | 10
         f_0(19, 23) -> 10*
         f_0(19, 22) -> 10*
         f_0(19, 21) -> 18* | 16 | 10
         f_0(19, 20) -> 18* | 16 | 10
         f_0(19, 19) -> 18* | 16 | 10
         f_0(19, 18) -> 10*
         f_0(19, 17) -> 18* | 16 | 10
         f_0(19, 16) -> 10*
         f_0(19, 15) -> 18* | 16 | 10
         f_0(19, 14) -> 10*
         f_0(19, 12) -> 18* | 16 | 10
         f_0(19, 10) -> 10*
          f_0(19, 9) -> 25* | 24 | 21 | 20 | 19 | 18 | 17 | 16 | 14 | 12 | 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) -> 10*
         f_0(18, 15) -> 22* | 14 | 10
         f_0(18, 14) -> 10*
         f_0(18, 12) -> 10*
         f_0(18, 10) -> 10*
          f_0(18, 9) -> 24* | 20 | 18 | 16 | 12
         f_0(17, 25) -> 18* | 16 | 10
         f_0(17, 24) -> 18* | 16 | 10
         f_0(17, 23) -> 10*
         f_0(17, 22) -> 10*
         f_0(17, 21) -> 18* | 16 | 10
         f_0(17, 20) -> 18* | 16 | 10
         f_0(17, 19) -> 18* | 16 | 10
         f_0(17, 18) -> 10*
         f_0(17, 17) -> 18* | 16 | 10
         f_0(17, 16) -> 10*
         f_0(17, 15) -> 18* | 16 | 10
         f_0(17, 14) -> 10*
         f_0(17, 12) -> 18* | 16 | 10
         f_0(17, 10) -> 10*
          f_0(17, 9) -> 19* | 17 | 14 | 12 | 10
         f_0(16, 25) -> 10*
         f_0(16, 24) -> 10*
         f_0(16, 23) -> 10*
         f_0(16, 22) -> 10*
         f_0(16, 21) -> 10*
         f_0(16, 20) -> 10*
         f_0(16, 19) -> 10*
         f_0(16, 18) -> 10*
         f_0(16, 17) -> 10*
         f_0(16, 16) -> 10*
         f_0(16, 15) -> 22* | 14 | 10
         f_0(16, 14) -> 10*
         f_0(16, 12) -> 10*
         f_0(16, 10) -> 10*
          f_0(16, 9) -> 12*
         f_0(15, 25) -> 18* | 16 | 10
         f_0(15, 24) -> 18* | 16 | 10
         f_0(15, 23) -> 10*
         f_0(15, 22) -> 10*
         f_0(15, 21) -> 18* | 16 | 10
         f_0(15, 20) -> 18* | 16 | 10
         f_0(15, 19) -> 18* | 16 | 10
         f_0(15, 18) -> 10*
         f_0(15, 17) -> 18* | 16 | 10
         f_0(15, 16) -> 10*
         f_0(15, 15) -> 16*
         f_0(15, 14) -> 10*
         f_0(15, 12) -> 16*
         f_0(15, 10) -> 10*
          f_0(15, 9) -> 12*
         f_0(14, 25) -> 18* | 16 | 10
         f_0(14, 24) -> 18* | 16 | 10
         f_0(14, 23) -> 10*
         f_0(14, 22) -> 10*
         f_0(14, 21) -> 18* | 16 | 10
         f_0(14, 20) -> 18* | 16 | 10
         f_0(14, 19) -> 18* | 16 | 10
         f_0(14, 18) -> 10*
         f_0(14, 17) -> 18* | 16 | 10
         f_0(14, 16) -> 10*
         f_0(14, 15) -> 16*
         f_0(14, 14) -> 10*
         f_0(14, 12) -> 16*
         f_0(14, 10) -> 10*
          f_0(14, 9) -> 12*
         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, 14) -> 10*
         f_0(12, 12) -> 10*
         f_0(12, 10) -> 10*
          f_0(12, 9) -> 19* | 17 | 14 | 12 | 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) -> 10*
         f_0(10, 15) -> 10*
         f_0(10, 14) -> 10*
         f_0(10, 12) -> 10*
         f_0(10, 10) -> 10*
          f_0(10, 9) -> 24* | 20 | 18 | 16 | 12
          f_0(9, 25) -> 14*
          f_0(9, 24) -> 14*
          f_0(9, 23) -> 14*
          f_0(9, 22) -> 14*
          f_0(9, 21) -> 14*
          f_0(9, 20) -> 14*
          f_0(9, 19) -> 14*
          f_0(9, 18) -> 14*
          f_0(9, 17) -> 14*
          f_0(9, 16) -> 14*
          f_0(9, 15) -> 14*
          f_0(9, 14) -> 14*
          f_0(9, 12) -> 14*
          f_0(9, 10) -> 14*
           f_0(9, 9) -> 15*}
      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 (1):
        Scc:
         {f#(y, f(x, f(a(), x))) -> f#(a(), y)}
        SCC (1):
         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:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [f](x0, x1) = x0 + 1,
           
           [a] = 0,
           
           [f#](x0, x1) = x0 + x1 + 1
          Strict:
           f#(y, f(x, f(a(), x))) -> f#(a(), y)
           2 + 1x + 1y >= 1 + 1y
          Weak:
           
         Qed