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