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