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