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