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