NO

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

Proof:
 String Reversal Processor:
  a(x1) -> x1
  a(x1) -> b(x1)
  c(b(a(x1))) -> a(c(a(b(c(x1)))))
  c(x1) -> x1
  DP Processor:
   DPs:
    c#(b(a(x1))) -> c#(x1)
    c#(b(a(x1))) -> a#(b(c(x1)))
    c#(b(a(x1))) -> c#(a(b(c(x1))))
    c#(b(a(x1))) -> a#(c(a(b(c(x1)))))
   TRS:
    a(x1) -> x1
    a(x1) -> b(x1)
    c(b(a(x1))) -> a(c(a(b(c(x1)))))
    c(x1) -> x1
   TDG Processor:
    DPs:
     c#(b(a(x1))) -> c#(x1)
     c#(b(a(x1))) -> a#(b(c(x1)))
     c#(b(a(x1))) -> c#(a(b(c(x1))))
     c#(b(a(x1))) -> a#(c(a(b(c(x1)))))
    TRS:
     a(x1) -> x1
     a(x1) -> b(x1)
     c(b(a(x1))) -> a(c(a(b(c(x1)))))
     c(x1) -> x1
    graph:
     c#(b(a(x1))) -> c#(a(b(c(x1)))) ->
     c#(b(a(x1))) -> a#(c(a(b(c(x1)))))
     c#(b(a(x1))) -> c#(a(b(c(x1)))) ->
     c#(b(a(x1))) -> c#(a(b(c(x1))))
     c#(b(a(x1))) -> c#(a(b(c(x1)))) -> c#(b(a(x1))) -> a#(b(c(x1)))
     c#(b(a(x1))) -> c#(a(b(c(x1)))) -> c#(b(a(x1))) -> c#(x1)
     c#(b(a(x1))) -> c#(x1) -> c#(b(a(x1))) -> a#(c(a(b(c(x1)))))
     c#(b(a(x1))) -> c#(x1) -> c#(b(a(x1))) -> c#(a(b(c(x1))))
     c#(b(a(x1))) -> c#(x1) -> c#(b(a(x1))) -> a#(b(c(x1)))
     c#(b(a(x1))) -> c#(x1) -> c#(b(a(x1))) -> c#(x1)
    SCC Processor:
     #sccs: 1
     #rules: 2
     #arcs: 8/16
     DPs:
      c#(b(a(x1))) -> c#(a(b(c(x1))))
      c#(b(a(x1))) -> c#(x1)
     TRS:
      a(x1) -> x1
      a(x1) -> b(x1)
      c(b(a(x1))) -> a(c(a(b(c(x1)))))
      c(x1) -> x1
     Loop Processor:
      loop length: 10
      terms:
       c(b(a(c(b(a(c(a(b(x1)))))))))
       c(b(a(a(c(a(b(c(c(a(b(x1)))))))))))
       c(b(a(a(c(a(b(c(a(b(x1))))))))))
       c(b(a(a(c(a(b(a(b(x1)))))))))
       c(b(a(a(a(b(a(b(x1))))))))
       a(c(a(b(c(a(a(b(a(b(x1))))))))))
       a(c(b(c(a(a(b(a(b(x1)))))))))
       a(c(b(c(b(a(b(a(b(x1)))))))))
       a(c(b(a(c(a(b(c(b(a(b(x1)))))))))))
       a(c(b(a(c(a(b(a(c(a(b(c(b(x1)))))))))))))
      context: a([])
      substitution:
       x1 -> c(b(x1))
      Qed