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

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