YES
TRS:
 {    f(x, f(y, z)) -> f(f(x, y), z),
  f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
 DP:
  Strict:
   {    f#(x, f(y, z)) -> f#(x, y),
        f#(x, f(y, z)) -> f#(f(x, y), z),
    f#(f(a(), a()), x) -> f#(a(), x),
    f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
    f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
  Weak:
  {    f(x, f(y, z)) -> f(f(x, y), z),
   f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
  EDG:
   {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), x))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
    (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), x))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))}
   SCCS:
    Scc:
     {    f#(x, f(y, z)) -> f#(x, y),
          f#(x, f(y, z)) -> f#(f(x, y), z),
      f#(f(a(), a()), x) -> f#(a(), x),
      f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
      f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
    SCC:
     Strict:
      {    f#(x, f(y, z)) -> f#(x, y),
           f#(x, f(y, z)) -> f#(f(x, y), z),
       f#(f(a(), a()), x) -> f#(a(), x),
       f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
       f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
     Weak:
     {    f(x, f(y, z)) -> f(f(x, y), z),
      f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
     POLY:
      Argument Filtering:
       pi(b) = [], pi(a) = [], pi(f#) = [0,1], pi(f) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [f#](x0, x1) = x0 + x1,
       [f](x0, x1) = x0 + x1,
       [b] = 0,
       [a] = 1
      Strict:
       {    f#(x, f(y, z)) -> f#(x, y),
            f#(x, f(y, z)) -> f#(f(x, y), z),
        f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
      Weak:
       {    f(x, f(y, z)) -> f(f(x, y), z),
        f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
      EDG:
       {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
        (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
        (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
        (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
        (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
        (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))}
       SCCS:
        Scc:
         {    f#(x, f(y, z)) -> f#(x, y),
              f#(x, f(y, z)) -> f#(f(x, y), z),
          f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
        SCC:
         Strict:
          {    f#(x, f(y, z)) -> f#(x, y),
               f#(x, f(y, z)) -> f#(f(x, y), z),
           f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
         Weak:
         {    f(x, f(y, z)) -> f(f(x, y), z),
          f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
         BOUND:
          Bound: match(-raise)-DP-bounded by 0
          Automaton:
           {      c_0() -> 4*
                  b_0() -> 3*
                  a_0() -> 2*
            f#_0(8, 10) -> 1*
             f#_0(8, 9) -> 1*
             f#_0(8, 6) -> 1*
             f#_0(8, 4) -> 1*
             f#_0(8, 3) -> 1*
             f#_0(7, 7) -> 1*
             f#_0(7, 5) -> 1*
             f#_0(7, 2) -> 1*
            f#_0(2, 10) -> 1*
             f#_0(2, 9) -> 1*
             f#_0(2, 6) -> 1*
             f#_0(2, 3) -> 1*
             f_0(10, 7) -> 10*
             f_0(10, 5) -> 6*
             f_0(10, 2) -> 6*
             f_0(9, 10) -> 10*
              f_0(9, 9) -> 6*
              f_0(9, 6) -> 6*
              f_0(9, 4) -> 6*
              f_0(9, 3) -> 10*
             f_0(8, 10) -> 7*
              f_0(8, 9) -> 8*
              f_0(8, 6) -> 8*
              f_0(8, 4) -> 8*
              f_0(8, 3) -> 7*
              f_0(7, 7) -> 7*
              f_0(7, 5) -> 8*
              f_0(7, 2) -> 8*
             f_0(6, 10) -> 10*
              f_0(6, 9) -> 6*
              f_0(6, 6) -> 6*
              f_0(6, 4) -> 6*
              f_0(6, 3) -> 10*
              f_0(5, 4) -> 5*
              f_0(3, 7) -> 10*
              f_0(3, 5) -> 6*
              f_0(3, 2) -> 9*
             f_0(2, 10) -> 7*
              f_0(2, 9) -> 8*
              f_0(2, 6) -> 8*
              f_0(2, 4) -> 5*
              f_0(2, 3) -> 7*
                      8 -> 5*}
          Strict:
           {f#(x, f(y, z)) -> f#(x, y),
            f#(x, f(y, z)) -> f#(f(x, y), z)}
          EDG:
           {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
            (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
            (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
            (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))}
           SCCS:
            Scc:
             {f#(x, f(y, z)) -> f#(x, y),
              f#(x, f(y, z)) -> f#(f(x, y), z)}
            SCC:
             Strict:
              {f#(x, f(y, z)) -> f#(x, y),
               f#(x, f(y, z)) -> f#(f(x, y), z)}
             Weak:
             {    f(x, f(y, z)) -> f(f(x, y), z),
              f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
             SPSC:
              Simple Projection:
               pi(f#) = 1
              Strict:
               {f#(x, f(y, z)) -> f#(f(x, y), z)}
              EDG:
               {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))}
               SCCS:
                Scc:
                 {f#(x, f(y, z)) -> f#(f(x, y), z)}
                SCC:
                 Strict:
                  {f#(x, f(y, z)) -> f#(f(x, y), z)}
                 Weak:
                 {    f(x, f(y, z)) -> f(f(x, y), z),
                  f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
                 SPSC:
                  Simple Projection:
                   pi(f#) = 1
                  Strict:
                   {}
                  Qed