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

Proof:
 Unfolding Processor:
  loop length: 7
  terms:
   a(a(a(a(c(a(a(a(c(a(a(c(a(x7473)))))))))))))
   a(c(a(c(c(c(a(a(a(c(a(a(c(a(x7473))))))))))))))
   a(c(a(a(a(a(a(a(a(c(a(a(c(a(x7473))))))))))))))
   a(c(a(a(a(a(c(a(c(c(c(a(a(c(a(x7473)))))))))))))))
   a(c(a(a(a(a(c(a(a(a(a(a(a(c(a(x7473)))))))))))))))
   a(c(a(a(a(a(c(a(a(a(c(a(c(c(c(a(x7473))))))))))))))))
   a(c(a(a(a(a(c(a(a(a(c(a(a(a(a(a(x7473))))))))))))))))
  context: a(c([]))
  substitution:
   x7473 -> c(c(x7473))
  Qed