Problem:
 a() -> c()
 c() -> a()
 c() -> h(a(),c())

Proof:
 Ground Confluence Processor:
  confluent by decision procedure.