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

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