YES

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

Proof:
 DP Processor:
  DPs:
   a#(x,y) -> c#(y)
   a#(x,y) -> b#(0(),c(y))
   a#(x,y) -> b#(x,b(0(),c(y)))
   c#(b(y,c(x))) -> a#(0(),0())
   c#(b(y,c(x))) -> b#(a(0(),0()),y)
   c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
   c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
  TRS:
   a(x,y) -> b(x,b(0(),c(y)))
   c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
   b(y,0()) -> y
  TDG Processor:
   DPs:
    a#(x,y) -> c#(y)
    a#(x,y) -> b#(0(),c(y))
    a#(x,y) -> b#(x,b(0(),c(y)))
    c#(b(y,c(x))) -> a#(0(),0())
    c#(b(y,c(x))) -> b#(a(0(),0()),y)
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
   TRS:
    a(x,y) -> b(x,b(0(),c(y)))
    c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
    b(y,0()) -> y
   graph:
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> b#(a(0(),0()),y)
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> a#(0(),0())
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> b#(a(0(),0()),y)
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> a#(0(),0())
    c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(x,b(0(),c(y)))
    c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(0(),c(y))
    c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> c#(y)
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> b#(a(0(),0()),y)
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> a#(0(),0())
   CDG Processor:
    DPs:
     a#(x,y) -> c#(y)
     a#(x,y) -> b#(0(),c(y))
     a#(x,y) -> b#(x,b(0(),c(y)))
     c#(b(y,c(x))) -> a#(0(),0())
     c#(b(y,c(x))) -> b#(a(0(),0()),y)
     c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
     c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
    TRS:
     a(x,y) -> b(x,b(0(),c(y)))
     c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
     b(y,0()) -> y
    graph:
     c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> c#(y)
     c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(0(),c(y))
     c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(x,b(0(),c(y)))
     a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> a#(0(),0())
     a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> b#(a(0(),0()),y)
     a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
     a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
    SCC Processor:
     #sccs: 1
     #rules: 2
     #arcs: 7/49
     DPs:
      c#(b(y,c(x))) -> a#(0(),0())
      a#(x,y) -> c#(y)
     TRS:
      a(x,y) -> b(x,b(0(),c(y)))
      c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
      b(y,0()) -> y
     KBO Processor:
      argument filtering:
       pi(a) = [0]
       pi(0) = []
       pi(c) = []
       pi(b) = [0]
       pi(a#) = [1]
       pi(c#) = [0]
      weight function:
       w0 = 1
       w(c#) = w(a#) = w(b) = w(c) = w(0) = w(a) = 1
      precedence:
       a# ~ 0 > a > c# ~ b ~ c
      problem:
       DPs:
        
       TRS:
        a(x,y) -> b(x,b(0(),c(y)))
        c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
        b(y,0()) -> y
      Qed