Problem:
 b() -> h(h(b(),a()),f(a()))
 h(h(a(),c()),b()) -> b()
 c() -> h(h(a(),h(a(),h(c(),b()))),f(f(h(h(a(),h(h(f(a()),c()),f(c()))),f(h(b(),a()))))))

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