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