NO Problem: b() -> a() b() -> c() c() -> b() c() -> d() Proof: Uncurry Processor: b() -> a() b() -> c() c() -> b() c() -> d() Ground Confluence Processor: non-confluent by decision procedure.