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