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