Problem:
 f(f(x)) -> g(x)

Proof:
 Nonconfluence Processor:
  terms: f(g(x4)) *<- f(f(f(x4))) ->* g(f(x4))
  Qed