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