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