YES

Problem:
 a(x1) -> b(x1)
 a(b(x1)) -> b(c(a(x1)))
 b(x1) -> c(x1)
 c(b(x1)) -> a(x1)

Proof:
 DP Processor:
  DPs:
   a#(x1) -> b#(x1)
   a#(b(x1)) -> a#(x1)
   a#(b(x1)) -> c#(a(x1))
   a#(b(x1)) -> b#(c(a(x1)))
   b#(x1) -> c#(x1)
   c#(b(x1)) -> a#(x1)
  TRS:
   a(x1) -> b(x1)
   a(b(x1)) -> b(c(a(x1)))
   b(x1) -> c(x1)
   c(b(x1)) -> a(x1)
  KBO Processor:
   weight function:
    w0 = 1
    w(c#) = w(b#) = w(a#) = w(b) = w(a) = 1
    w(c) = 0
   precedence:
    c > a# > b# > a > c# ~ b
   problem:
    DPs:
     
    TRS:
     
   Qed