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