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