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

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