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

Proof:
 Ground Confluence Processor:
  non-confluent by decision procedure.