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

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