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

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