Problem:
 a(x) -> b(x)
 a(x) -> c(c(x))
 b(x) -> g(b(x))
 c(x) -> c(x)

Proof:
 Nonconfluence Processor:
  terms: b(x) *<- a(x) ->* c(c(x))
  Qed