NO

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

Proof:
 DP Processor:
  DPs:
   a#(a(b(c(x1)))) -> a#(x1)
   a#(a(b(c(x1)))) -> a#(a(x1))
   a#(a(b(c(x1)))) -> a#(a(a(x1)))
  TRS:
   a(x1) -> b(x1)
   a(a(b(c(x1)))) -> b(c(c(a(a(a(x1))))))
  Loop Processor:
   loop length: 13
   terms:
    a(a(b(c(c(a(a(b(c(b(c(c(a(a(a(a(x1))))))))))))))))
    b(c(c(a(a(a(c(a(a(b(c(b(c(c(a(a(a(a(x1))))))))))))))))))
    b(c(c(a(a(a(c(a(a(b(c(b(c(c(a(b(a(a(x1))))))))))))))))))
    b(c(c(a(a(a(c(b(c(c(a(a(a(b(c(c(a(b(a(a(x1))))))))))))))))))))
    b(c(c(a(a(b(c(b(c(c(a(a(a(b(c(c(a(b(a(a(x1))))))))))))))))))))
    b(c(c(b(c(c(a(a(a(b(c(c(a(a(a(b(c(c(a(b(a(a(x1))))))))))))))))))))))
    b(c(c(b(c(c(a(b(c(c(a(a(a(c(a(a(a(b(c(c(a(b(a(a(x1))))))))))))))))))))))))
    b(c(c(b(c(c(a(b(c(c(a(a(b(c(a(a(a(b(c(c(a(b(a(a(x1))))))))))))))))))))))))
    b(c(c(b(c(c(a(b(c(c(b(c(c(a(a(a(a(a(a(b(c(c(a(b(a(a(x1))))))))))))))))))))))))))
    b(c(c(b(c(c(a(b(c(c(b(c(c(a(a(a(a(b(c(c(a(a(a(c(a(b(a(a(x1))))))))))))))))))))))))))))
    b(c(c(b(c(c(a(b(c(c(b(c(c(a(a(a(a(b(c(c(a(a(b(c(a(b(a(a(x1))))))))))))))))))))))))))))
    b(c(c(b(c(c(a(b(c(c(b(c(c(a(a(b(c(c(a(a(a(c(a(a(b(c(a(b(a(a(x1))))))))))))))))))))))))))))))
    b(c(c(b(c(c(a(b(c(c(b(c(c(a(a(b(c(c(a(a(b(c(a(a(b(c(a(b(a(a(x1))))))))))))))))))))))))))))))
   context: b(c(c(b(c(c(a(b(c(c(b(c(c([])))))))))))))
   substitution:
    x1 -> b(a(a(x1)))
   Qed