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