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