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