YES

Problem:
 c(c(c(y))) -> c(c(a(y,0())))
 c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
 c(y) -> y

Proof:
 DP Processor:
  DPs:
   c#(c(c(y))) -> c#(a(y,0()))
   c#(c(c(y))) -> c#(c(a(y,0())))
   c#(a(a(0(),x),y)) -> c#(0())
   c#(a(a(0(),x),y)) -> c#(c(0()))
   c#(a(a(0(),x),y)) -> c#(c(c(0())))
  TRS:
   c(c(c(y))) -> c(c(a(y,0())))
   c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
   c(y) -> y
  EDG Processor:
   DPs:
    c#(c(c(y))) -> c#(a(y,0()))
    c#(c(c(y))) -> c#(c(a(y,0())))
    c#(a(a(0(),x),y)) -> c#(0())
    c#(a(a(0(),x),y)) -> c#(c(0()))
    c#(a(a(0(),x),y)) -> c#(c(c(0())))
   TRS:
    c(c(c(y))) -> c(c(a(y,0())))
    c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
    c(y) -> y
   graph:
    c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(c(c(y))) -> c#(a(y,0()))
    c#(a(a(0(),x),y)) -> c#(c(0())) ->
    c#(c(c(y))) -> c#(c(a(y,0())))
    c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(a(a(0(),x),y)) -> c#(0())
    c#(a(a(0(),x),y)) -> c#(c(0())) ->
    c#(a(a(0(),x),y)) -> c#(c(0()))
    c#(a(a(0(),x),y)) -> c#(c(0())) ->
    c#(a(a(0(),x),y)) -> c#(c(c(0())))
    c#(a(a(0(),x),y)) -> c#(c(c(0()))) ->
    c#(c(c(y))) -> c#(a(y,0()))
    c#(a(a(0(),x),y)) -> c#(c(c(0()))) ->
    c#(c(c(y))) -> c#(c(a(y,0())))
    c#(a(a(0(),x),y)) -> c#(c(c(0()))) ->
    c#(a(a(0(),x),y)) -> c#(0())
    c#(a(a(0(),x),y)) -> c#(c(c(0()))) ->
    c#(a(a(0(),x),y)) -> c#(c(0()))
    c#(a(a(0(),x),y)) -> c#(c(c(0()))) ->
    c#(a(a(0(),x),y)) -> c#(c(c(0())))
    c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(0())
    c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(c(0()))
    c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(c(c(0())))
    c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(c(c(y))) -> c#(a(y,0()))
    c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(c(c(y))) -> c#(c(a(y,0())))
    c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(0())
    c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(c(0()))
    c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(c(c(0())))
   SCC Processor:
    #sccs: 1
    #rules: 4
    #arcs: 18/25
    DPs:
     c#(a(a(0(),x),y)) -> c#(c(0()))
     c#(a(a(0(),x),y)) -> c#(c(c(0())))
     c#(c(c(y))) -> c#(c(a(y,0())))
     c#(c(c(y))) -> c#(a(y,0()))
    TRS:
     c(c(c(y))) -> c(c(a(y,0())))
     c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
     c(y) -> y
    Bounds Processor:
     bound: 5
     enrichment: match
     automaton:
      final states: {6}
      transitions:
       a3(5,11) -> 12*
       a3(5,17) -> 19*
       a3(11,17) -> 18*
       03() -> 17*
       c{#,3}(19) -> 6*
       c{#,3}(18) -> 6*
       c4(25) -> 10,5
       c4(24) -> 25*
       c4(23) -> 24*
       a4(5,17) -> 10*
       a4(17,23) -> 24*
       c{#,0}(5) -> 6*
       04() -> 23*
       a0(5,5) -> 5*
       c{#,4}(25) -> 6*
       c{#,4}(24) -> 6*
       00() -> 5*
       c5(30) -> 31*
       c5(31) -> 10,5
       c0(5) -> 5*
       a5(23,29) -> 30*
       a1(23,9) -> 9*
       a1(18,9) -> 9*
       a1(13,9) -> 9*
       a1(30,9) -> 9*
       a1(25,9) -> 9*
       a1(5,5) -> 5*
       a1(10,9) -> 9*
       a1(5,9) -> 10,9
       a1(17,9) -> 9*
       a1(12,9) -> 9*
       a1(24,9) -> 9*
       a1(19,9) -> 9*
       a1(9,9) -> 9*
       a1(31,9) -> 9*
       a1(11,9) -> 9*
       05() -> 29*
       c1(10) -> 5,10
       c1(9) -> 10*
       c{#,5}(30) -> 6*
       c{#,5}(31) -> 6*
       01() -> 9*
       c{#,1}(10) -> 6*
       c{#,1}(9) -> 6*
       c2(12) -> 10,5,13
       c2(11) -> 12*
       c2(13) -> 10,5
       a2(23,11) -> 11*
       a2(18,11) -> 11*
       a2(13,11) -> 11*
       a2(30,11) -> 11*
       a2(25,11) -> 11*
       a2(5,9) -> 10*
       a2(10,11) -> 12*
       a2(5,11) -> 13*
       a2(17,11) -> 11*
       a2(12,11) -> 11*
       a2(24,11) -> 11*
       a2(19,11) -> 11*
       a2(9,11) -> 12*
       a2(31,11) -> 11*
       a2(11,11) -> 11*
       02() -> 11*
       c{#,2}(12) -> 6*
       c{#,2}(11) -> 6*
       c{#,2}(13) -> 6*
       c3(17) -> 18*
       c3(19) -> 10,5
       c3(18) -> 19*
       9 -> 10*
       10 -> 5*
       11 -> 12,13,10
       12 -> 13*
       13 -> 10*
       17 -> 18,19
       18 -> 19*
       19 -> 10*
       23 -> 24,25
       24 -> 25*
       25 -> 10,5
       30 -> 31*
       31 -> 10*
     problem:
      DPs:
       
      TRS:
       c(c(c(y))) -> c(c(a(y,0())))
       c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
       c(y) -> y
     Qed