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

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