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

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