YES
TRS:
 {            f(x, f(y, z)) -> f(f(x, y), z),
  f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), 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(f(a(), b()), c()), x) -> f#(b(), x),
    f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))),
    f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))),
    f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))}
  Weak:
  {            f(x, f(y, z)) -> f(f(x, y), z),
   f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))}
  EDG:
   {(f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))))
    (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(b(), x))
    (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#(x, f(y, z)) -> f#(x, y))
    (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(f(f(a(), b()), c()), x) -> f#(b(), x), 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#(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(f(a(), b()), c()), x) -> f#(b(), x))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))))
    (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)))
    (f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(x, f(y, z)) -> f#(f(x, y), z))
    (f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)), f#(x, f(y, z)) -> f#(x, y))
    (f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), 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(f(a(), b()), c()), x) -> f#(b(), x),
      f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))),
      f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))),
      f#(f(f(a(), b()), c()), x) -> f#(c(), 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(f(a(), b()), c()), x) -> f#(b(), x),
       f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))),
       f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))),
       f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))}
     Weak:
     {            f(x, f(y, z)) -> f(f(x, y), z),
      f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))}
     POLY:
      Argument Filtering:
       pi(c) = [], pi(a) = [], pi(b) = [], pi(f#) = 0, pi(f) = 0
      Usable Rules:
       {}
      Interpretation:
       [c] = 0,
       [a] = 1,
       [b] = 0
      Strict:
       {            f#(x, f(y, z)) -> f#(x, y),
                    f#(x, f(y, z)) -> f#(f(x, y), z),
        f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))}
      Weak:
       {            f(x, f(y, z)) -> f(f(x, y), z),
        f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))}
      EDG:
       {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), 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#(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(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))))
        (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(x, y))
        (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), 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(f(a(), b()), c()), x) -> f#(a(), f(c(), 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(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))}
         Weak:
         {            f(x, f(y, z)) -> f(f(x, y), z),
          f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))}
         BOUND:
          Bound: match(-raise)-DP-bounded by 1
          Automaton:
           {       c_1() -> 16*
                   c_0() -> 12*
                   a_1() -> 15*
                   a_0() -> 11*
                   b_1() -> 17*
                   b_0() -> 10*
            f#_1(21, 14) -> 6*
            f#_1(21, 13) -> 6*
            f#_1(21, 12) -> 6*
            f#_1(21, 11) -> 6*
            f#_1(21, 10) -> 6*
             f#_1(21, 9) -> 6*
            f#_1(20, 18) -> 6*
            f#_1(20, 17) -> 6*
            f#_1(15, 22) -> 6*
            f#_1(15, 19) -> 6*
            f#_1(15, 16) -> 6*
            f#_0(11, 14) -> 6*
            f#_0(11, 13) -> 6*
            f#_0(11, 12) -> 6*
            f#_0(11, 11) -> 6*
            f#_0(11, 10) -> 6*
             f#_0(11, 9) -> 6*
             f#_0(9, 14) -> 6*
             f#_0(9, 13) -> 6*
             f#_0(9, 12) -> 6*
             f#_0(9, 11) -> 6*
             f#_0(9, 10) -> 6*
              f#_0(9, 9) -> 6*
             f_1(22, 14) -> 19*
             f_1(22, 13) -> 19*
             f_1(22, 12) -> 19*
             f_1(22, 11) -> 19*
             f_1(22, 10) -> 19*
              f_1(22, 9) -> 19*
             f_1(21, 14) -> 21*
             f_1(21, 13) -> 21*
             f_1(21, 12) -> 21*
             f_1(21, 11) -> 21*
             f_1(21, 10) -> 21*
              f_1(21, 9) -> 21*
             f_1(20, 18) -> 21*
             f_1(20, 17) -> 21*
             f_1(19, 14) -> 19*
             f_1(19, 13) -> 19*
             f_1(19, 12) -> 19*
             f_1(19, 11) -> 19*
             f_1(19, 10) -> 19*
              f_1(19, 9) -> 19*
             f_1(18, 14) -> 18*
             f_1(18, 13) -> 18*
             f_1(18, 12) -> 18*
             f_1(18, 11) -> 18*
             f_1(18, 10) -> 18*
              f_1(18, 9) -> 18*
             f_1(17, 14) -> 18*
             f_1(17, 13) -> 18*
             f_1(17, 12) -> 18*
             f_1(17, 11) -> 18*
             f_1(17, 10) -> 18*
              f_1(17, 9) -> 18*
             f_1(16, 18) -> 19*
             f_1(16, 17) -> 22*
             f_1(15, 22) -> 21*
             f_1(15, 19) -> 21*
             f_1(15, 16) -> 20*
             f_0(14, 14) -> 14 | 9
             f_0(14, 13) -> 14 | 9
             f_0(14, 12) -> 14 | 9
             f_0(14, 11) -> 14 | 9
             f_0(14, 10) -> 14 | 9
              f_0(14, 9) -> 14 | 9
             f_0(13, 14) -> 14 | 13 | 9
             f_0(13, 13) -> 14 | 13 | 9
             f_0(13, 12) -> 14 | 13 | 9
             f_0(13, 11) -> 14 | 13 | 9
             f_0(13, 10) -> 14 | 13 | 9
              f_0(13, 9) -> 14 | 13 | 9
             f_0(12, 14) -> 9*
             f_0(12, 13) -> 14*
             f_0(12, 12) -> 9*
             f_0(12, 11) -> 9*
             f_0(12, 10) -> 9*
              f_0(12, 9) -> 9*
             f_0(11, 14) -> 9*
             f_0(11, 13) -> 9*
             f_0(11, 12) -> 9*
             f_0(11, 11) -> 9*
             f_0(11, 10) -> 9*
              f_0(11, 9) -> 9*
             f_0(10, 14) -> 13*
             f_0(10, 13) -> 13*
             f_0(10, 12) -> 13*
             f_0(10, 11) -> 13*
             f_0(10, 10) -> 13*
              f_0(10, 9) -> 14 | 13 | 9
              f_0(9, 14) -> 14 | 9
              f_0(9, 13) -> 14 | 9
              f_0(9, 12) -> 14 | 9
              f_0(9, 11) -> 14 | 9
              f_0(9, 10) -> 14 | 9
               f_0(9, 9) -> 14 | 9}
          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(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), 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(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))}
                 SPSC:
                  Simple Projection:
                   pi(f#) = 1
                  Strict:
                   {}
                  Qed