Problem:
 F(x) -> A()
 F(x) -> G(F(x))
 G(F(x)) -> F(H(x))
 G(F(x)) -> B()

Proof:
 Nonconfluence Processor:
  terms: G(A()) *<- G(F(x)) ->* B()
  Qed