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