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

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