YES
Trs:
 {     c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))),
        a(y, 0()) -> b(y, 0()),
  b(b(0(), y), x) -> y}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {    c_1(q10) -> q4,
          c_1(q9) -> q10,
          c_1(q6) -> q7,
          c_0(q4) -> q4,
      a_1(q8, q5) -> q9,
      a_1(q7, q5) -> q8,
      a_0(q4, q4) -> q4,
            0_2() -> q11,
            0_1() -> q5,
            0_0() -> q4,
     b_2(q8, q11) -> q9,
     b_2(q7, q11) -> q8,
     b_1(q5, q10) -> q6,
      b_1(q5, q9) -> q6,
      b_1(q5, q4) -> q6,
      b_1(q4, q5) -> q4,
      b_0(q4, q4) -> q4,
               q5 -> q4}
   Strict:
   {}
   Qed