YES

Problem:
 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())

Proof:
 DP Processor:
  DPs:
   c#(c(c(y))) -> b#(0(),y)
   c#(c(c(y))) -> c#(b(0(),y))
   c#(c(c(y))) -> a#(c(b(0(),y)),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))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
   a#(y,0()) -> b#(y,0())
  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())
  EDG Processor:
   DPs:
    c#(c(c(y))) -> b#(0(),y)
    c#(c(c(y))) -> c#(b(0(),y))
    c#(c(c(y))) -> a#(c(b(0(),y)),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))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
    a#(y,0()) -> b#(y,0())
   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())
   graph:
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0()) ->
    a#(y,0()) -> b#(y,0())
    c#(c(c(y))) -> a#(c(b(0(),y)),0()) ->
    a#(y,0()) -> b#(y,0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> b#(0(),y)
    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))) -> a#(c(b(0(),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))) -> 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#(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))) -> 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())
    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))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 14/49
    DPs:
     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())))
    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())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [c#](x0) = x0,
      
      [a](x0, x1) = x0,
      
      [c](x0) = x0 + 1,
      
      [b](x0, x1) = x0 + x1,
      
      [0] = 0
     orientation:
      c#(c(c(y))) = y + 2 >= y + 1 = c#(a(a(c(b(0(),y)),0()),0()))
      
      c#(c(c(y))) = y + 2 >= y + 2 = c#(c(a(a(c(b(0(),y)),0()),0())))
      
      b(b(0(),y),x) = x + y >= y = y
      
      c(c(c(y))) = y + 3 >= y + 3 = c(c(a(a(c(b(0(),y)),0()),0())))
      
      a(y,0()) = y >= y = b(y,0())
     problem:
      DPs:
       c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
      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())
     Bounds Processor:
      bound: 2
      enrichment: match
      automaton:
       final states: {7}
       transitions:
        b0(6,6) -> 6*
        00() -> 6*
        b1(14,6) -> 15*
        b1(14,18) -> 15*
        b1(6,14) -> 6*
        b1(14,19) -> 15*
        01() -> 14*
        c1(15) -> 16*
        c1(19) -> 6*
        c1(18) -> 19*
        a1(17,14) -> 18*
        a1(16,14) -> 17*
        c{#,1}(19) -> 7*
        b2(17,20) -> 18*
        b2(16,20) -> 17*
        c{#,0}(6) -> 7*
        02() -> 20*
        c0(6) -> 6*
        a0(6,6) -> 6*
        14 -> 6*
      problem:
       DPs:
        
       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())
      Qed