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