YES
TRS:
 {    f(x, f(y, z)) -> f(f(x, y), z),
  f(f(a(), b()), x) -> f(a(), f(a(), x)),
  f(f(b(), a()), x) -> f(b(), f(b(), x))}
 DP:
  Strict:
   {    f#(x, f(y, z)) -> f#(x, y),
        f#(x, f(y, z)) -> f#(f(x, y), z),
    f#(f(a(), b()), x) -> f#(a(), x),
    f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
    f#(f(b(), a()), x) -> f#(b(), x),
    f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
  Weak:
  {    f(x, f(y, z)) -> f(f(x, y), z),
   f(f(a(), b()), x) -> f(a(), f(a(), x)),
   f(f(b(), a()), x) -> f(b(), f(b(), x))}
  EDG:
   {(f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(x, y))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x)))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), x))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), x)))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), 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(b(), a()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(f(b(), a()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(a(), b()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(a(), b()), 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(), b()), x) -> f#(a(), x))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(a(), f(a(), x)))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(b(), a()), x) -> f#(b(), x))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(b(), a()), x) -> f#(b(), f(b(), x)))
    (f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(a(), b()), x) -> f#(a(), 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(), b()), x) -> f#(a(), x),
      f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
      f#(f(b(), a()), x) -> f#(b(), x),
      f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
    SCC:
     Strict:
      {    f#(x, f(y, z)) -> f#(x, y),
           f#(x, f(y, z)) -> f#(f(x, y), z),
       f#(f(a(), b()), x) -> f#(a(), x),
       f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
       f#(f(b(), a()), x) -> f#(b(), x),
       f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
     Weak:
     {    f(x, f(y, z)) -> f(f(x, y), z),
      f(f(a(), b()), x) -> f(a(), f(a(), x)),
      f(f(b(), a()), x) -> f(b(), f(b(), 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 + 1,
       [b] = 0,
       [a] = 0
      Strict:
       {    f#(x, f(y, z)) -> f#(f(x, y), z),
        f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
        f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
      Weak:
       {    f(x, f(y, z)) -> f(f(x, y), z),
        f(f(a(), b()), x) -> f(a(), f(a(), x)),
        f(f(b(), a()), x) -> f(b(), f(b(), x))}
      EDG:
       {(f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(f(b(), a()), x) -> f#(b(), f(b(), 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#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), x)))
        (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x)))}
       SCCS:
        Scc:
         {    f#(x, f(y, z)) -> f#(f(x, y), z),
          f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
          f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
        SCC:
         Strict:
          {    f#(x, f(y, z)) -> f#(f(x, y), z),
           f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
           f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
         Weak:
         {    f(x, f(y, z)) -> f(f(x, y), z),
          f(f(a(), b()), x) -> f(a(), f(a(), x)),
          f(f(b(), a()), x) -> f(b(), f(b(), x))}
         UR:
          {    f(x, f(y, z)) -> f(f(x, y), z),
           f(f(a(), b()), x) -> f(a(), f(a(), x)),
           f(f(b(), a()), x) -> f(b(), f(b(), x))}
          BOUND:
           Bound: match(-raise)-DP-bounded by 0
           Automaton:
            {     c_0() -> 3*
                  a_0() -> 2*
             f#_0(5, 4) -> 1*
             f#_0(5, 3) -> 1*
             f#_0(5, 2) -> 1*
             f#_0(2, 4) -> 1*
              f_0(5, 4) -> 5*
              f_0(5, 3) -> 5*
              f_0(5, 2) -> 5*
              f_0(4, 3) -> 4*
              f_0(2, 4) -> 5*
              f_0(2, 3) -> 4*
              f_0(2, 2) -> 5*
                      5 -> 4*}
           Strict:
            {    f#(x, f(y, z)) -> f#(f(x, y), z),
             f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
           EDG:
            {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x)))
             (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
             (f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))}
            SCCS:
             Scc:
              {    f#(x, f(y, z)) -> f#(f(x, y), z),
               f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
             SCC:
              Strict:
               {    f#(x, f(y, z)) -> f#(f(x, y), z),
                f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
              Weak:
              {    f(x, f(y, z)) -> f(f(x, y), z),
               f(f(a(), b()), x) -> f(a(), f(a(), x)),
               f(f(b(), a()), x) -> f(b(), f(b(), x))}
              UR:
               {    f(x, f(y, z)) -> f(f(x, y), z),
                f(f(a(), b()), x) -> f(a(), f(a(), x)),
                f(f(b(), a()), x) -> f(b(), f(b(), x))}
               BOUND:
                Bound: match(-raise)-DP-bounded by 0
                Automaton:
                 {     d_0() -> 3*
                       b_0() -> 2*
                  f#_0(5, 4) -> 1*
                  f#_0(5, 3) -> 1*
                  f#_0(5, 2) -> 1*
                  f#_0(2, 4) -> 1*
                   f_0(5, 4) -> 5*
                   f_0(5, 3) -> 5*
                   f_0(5, 2) -> 5*
                   f_0(4, 3) -> 4*
                   f_0(2, 4) -> 5*
                   f_0(2, 3) -> 4*
                   f_0(2, 2) -> 5*
                           5 -> 4*}
                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(), b()), x) -> f(a(), f(a(), x)),
                    f(f(b(), a()), x) -> f(b(), f(b(), x))}
                   SPSC:
                    Simple Projection:
                     pi(f#) = 1
                    Strict:
                     {}
                    Qed