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