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

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