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