NO Problem: b() -> c() h(b(),b()) -> a() h(c(),c()) -> c() c() -> c() Proof: Ground Confluence Processor: not UNC by decision procedure.