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