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

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