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())}
         UR:
          {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 2
           Automaton:
            {a_1(5, 2) -> 6*
             a_1(4, 2) -> 5*
             a_0(1, 1) -> 1*
               c#_1(7) -> 1*
               c#_0(1) -> 1*
                c_1(7) -> 1*
                c_1(6) -> 7*
                c_1(3) -> 4*
                c_0(1) -> 1*
                 0_2() -> 8*
                 0_1() -> 2*
                 0_0() -> 1*
             b_2(5, 8) -> 6*
             b_2(4, 8) -> 5*
             b_1(2, 7) -> 3*
             b_1(2, 6) -> 3*
             b_1(2, 1) -> 3*
             b_1(1, 2) -> 1*
             b_0(1, 1) -> 1*
                     2 -> 1*}
           Strict:
            {}
           Qed