Successfully proved nontermination of
a(c(x)) -> b(x)
a(a(b(x))) -> a(c(c(a(a(a(x))))))