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

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