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

Proof:
 Nonconfluence Processor:
  terms: H(K(f2())) *<- H(H(H(f2()))) ->* K(H(f2()))
  Qed
  
  first automaton:
   final states: {1}
   transitions:
    H(3) -> 1*
    K(2) -> 3*
    f2() -> 2*
  
  second automaton:
   final states: {4}
   transitions:
    H(5) -> 6*
    K(6) -> 4*
    f2() -> 5*