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