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