YES
TRS:
 {b(a(), f(b(b(z, y), a()))) -> z,
          f(f(c(a(), y, z))) -> b(y, b(z, z)),
     c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x)))))}
 DP:
  Strict:
   {     f#(f(c(a(), y, z))) -> b#(z, z),
         f#(f(c(a(), y, z))) -> b#(y, b(z, z)),
    c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))),
    c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)),
    c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))),
    c#(c(z, x, a()), a(), y) -> c#(z, y, x),
    c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x)))}
  Weak:
  {b(a(), f(b(b(z, y), a()))) -> z,
           f(f(c(a(), y, z))) -> b(y, b(z, z)),
      c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x)))))}
  EDG:
   {(c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)), f#(f(c(a(), y, z))) -> b#(y, b(z, z)))
    (c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)), f#(f(c(a(), y, z))) -> b#(z, z))
    (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))))
    (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(z, y, x))
    (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))))
    (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)))
    (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))))
    (c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))), f#(f(c(a(), y, z))) -> b#(z, z))
    (c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))), f#(f(c(a(), y, z))) -> b#(y, b(z, z)))
    (c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))), f#(f(c(a(), y, z))) -> b#(z, z))
    (c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))), f#(f(c(a(), y, z))) -> b#(y, b(z, z)))
    (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))))
    (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)))
    (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))))
    (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> c#(z, y, x))
    (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))))}
   SCCS:
    Scc:
     {c#(c(z, x, a()), a(), y) -> c#(z, y, x),
      c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x)))}
    SCC:
     Strict:
      {c#(c(z, x, a()), a(), y) -> c#(z, y, x),
       c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x)))}
     Weak:
     {b(a(), f(b(b(z, y), a()))) -> z,
              f(f(c(a(), y, z))) -> b(y, b(z, z)),
         c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x)))))}
     UR:
      {b(a(), f(b(b(z, y), a()))) -> z,
               f(f(c(a(), y, z))) -> b(y, b(z, z)),
          c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x))))),
                          d(w, v) -> w,
                          d(w, v) -> v}
      BOUND:
       Bound: top(-raise)-DP-bounded by 2
       Automaton:
        {       d_0(8, 8) -> 6*
                d_0(8, 7) -> 6*
                d_0(8, 6) -> 6*
                d_0(7, 8) -> 6*
                d_0(7, 7) -> 6*
                d_0(7, 6) -> 6*
                d_0(6, 8) -> 6*
                d_0(6, 7) -> 6*
                d_0(6, 6) -> 6*
         c#_2(11, 12, 14) -> 3*
           c#_1(8, 9, 11) -> 3*
           c#_1(6, 11, 6) -> 3*
            c#_0(8, 8, 8) -> 3*
            c#_0(8, 8, 7) -> 3*
            c#_0(8, 8, 6) -> 3*
            c#_0(8, 7, 8) -> 3*
            c#_0(8, 6, 8) -> 3*
            c#_0(7, 8, 8) -> 3*
            c#_0(7, 8, 7) -> 3*
            c#_0(7, 8, 6) -> 3*
            c#_0(7, 7, 8) -> 3*
            c#_0(7, 6, 8) -> 3*
            c#_0(6, 8, 8) -> 3*
            c#_0(6, 8, 7) -> 3*
            c#_0(6, 8, 6) -> 3*
            c#_0(6, 7, 8) -> 3*
            c#_0(6, 6, 8) -> 3*
            c_2(6, 11, 6) -> 13*
           c_1(11, 9, 19) -> 20*
             c_1(8, 8, 8) -> 10*
             c_1(8, 8, 7) -> 10*
             c_1(8, 8, 6) -> 10*
             c_1(7, 8, 8) -> 10*
             c_1(7, 8, 7) -> 10*
             c_1(7, 8, 6) -> 10*
            c_1(6, 11, 6) -> 18*
            c_1(6, 9, 11) -> 15*
             c_1(6, 8, 8) -> 10*
             c_1(6, 8, 7) -> 10*
             c_1(6, 8, 6) -> 10*
             c_0(8, 8, 8) -> 7*
             c_0(8, 8, 7) -> 7*
             c_0(8, 8, 6) -> 7*
             c_0(8, 7, 8) -> 7*
             c_0(8, 7, 7) -> 7*
             c_0(8, 7, 6) -> 7*
             c_0(8, 6, 8) -> 7*
             c_0(8, 6, 7) -> 7*
             c_0(8, 6, 6) -> 7*
             c_0(7, 8, 8) -> 7*
             c_0(7, 8, 7) -> 7*
             c_0(7, 8, 6) -> 7*
             c_0(7, 7, 8) -> 7*
             c_0(7, 7, 7) -> 7*
             c_0(7, 7, 6) -> 7*
             c_0(7, 6, 8) -> 7*
             c_0(7, 6, 7) -> 7*
             c_0(7, 6, 6) -> 7*
             c_0(6, 8, 8) -> 7*
             c_0(6, 8, 7) -> 7*
             c_0(6, 8, 6) -> 7*
             c_0(6, 7, 8) -> 7*
             c_0(6, 7, 7) -> 7*
             c_0(6, 7, 6) -> 7*
             c_0(6, 6, 8) -> 7*
             c_0(6, 6, 7) -> 7*
             c_0(6, 6, 6) -> 7*
                  f_2(13) -> 14*
                  f_1(21) -> 15*
                  f_1(20) -> 21*
                  f_1(18) -> 19*
                  f_1(16) -> 10*
                  f_1(15) -> 16*
                  f_1(10) -> 11*
                   f_0(8) -> 6*
                   f_0(7) -> 8*
                   f_0(6) -> 7 | 6
                    a_2() -> 12*
                    a_1() -> 9*
                    a_0() -> 6*
              b_1(11, 11) -> 17*
               b_1(9, 17) -> 10*
                b_0(8, 8) -> 6*
                b_0(8, 7) -> 6*
                b_0(8, 6) -> 6*
                b_0(7, 8) -> 6*
                b_0(7, 7) -> 6*
                b_0(7, 6) -> 6*
                b_0(6, 8) -> 6*
                b_0(6, 7) -> 6*
                b_0(6, 6) -> 8 | 7 | 6
                        8 -> 6*
                        7 -> 6*
                        6 -> 8 | 7}
       Strict:
        {c#(c(z, x, a()), a(), y) -> c#(z, y, x)}
       EDG:
        {(c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(z, y, x))}
        SCCS:
         Scc:
          {c#(c(z, x, a()), a(), y) -> c#(z, y, x)}
         SCC:
          Strict:
           {c#(c(z, x, a()), a(), y) -> c#(z, y, x)}
          Weak:
          {b(a(), f(b(b(z, y), a()))) -> z,
                   f(f(c(a(), y, z))) -> b(y, b(z, z)),
              c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x)))))}
          SPSC:
           Simple Projection:
            pi(c#) = 0
           Strict:
            {}
           Qed