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