Problem:
 H(H(x)) -> K(x)

Proof:
 Nonconfluence Processor:
  terms: H(K(x3)) *<- H(H(H(x3))) ->* K(H(x3))
  Qed