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