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