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