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:
 Uncurry Processor:
  b() -> f5(f5(h(),f5(f5(h(),b()),a())),f5(f(),a()))
  f5(f5(h(),f5(f5(h(),a()),c())),b()) -> b()
  c() ->
  f5(f5(h(),f5(f5(h(),a()),f5(f5(h(),a()),f5(f5(h(),c()),b())))),f5(f(),
                                                                    f5
                                                                    (
                                                                    f(),
                                                                    f5
                                                                    (
                                                                    f5
                                                                    (
                                                                    h(),
                                                                    f5
                                                                    (
                                                                    f5(h(),a()),
                                                                    f5
                                                                    (
                                                                    f5
                                                                    (
                                                                    h(),
                                                                    f5(f5(h(),f5(f(),a())),c())),
                                                                    f5
                                                                    (f(),c())))),
                                                                    f5
                                                                    (f(),f5(f5(h(),b()),a()))))))
  Ground Confluence Processor:
   non-confluent by decision procedure.