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