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