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