NO

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

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