Problem:
 F(x,x) -> A()
 F(x,G(x)) -> B()
 C() -> G(C())

Proof:
 Nonconfluence Processor:
  terms: B() *<- F(C(),C()) ->* A()
  Qed