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

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