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

Proof:
 Uncurry Processor:
  b() -> f5(f(),b())
  f5(f5(h(),f5(f5(h(),f5(f5(h(),f5(f5(h(),f5(f5(h(),f5(f5(h(),f5(f5(h(),a()),
                                                                 f5(f5(h(),c()),
                                                                    f5
                                                                    (f5(h(),f5(f(),c())),b())))),
                                                       f5(f5(h(),b()),
                                                          f5(f5(h(),b()),
                                                             f5(f5(h(),
                                                                   f5
                                                                   (f(),f5(f(),f5(f5(h(),c()),b())))),
                                                                a()))))),
                                             f5(f5(h(),a()),a()))),b())),
                         f5(f(),f5(f5(h(),f5(f5(h(),f5(f(),a())),a())),c())))),
               a())),f5(f5(h(),c()),a()))
  -> f5(f(),a())
  c() -> f5(f5(h(),b()),b())
  Ground Confluence Processor:
   non-confluent by decision procedure.