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

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