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