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