YES Problem: b() -> h(b(),a()) b() -> h(f(b()),f(h(b(),a()))) Proof: Uncurry Processor: b() -> f4(f4(h(),b()),a()) b() -> f4(f4(h(),f4(f(),b())),f4(f(),f4(f4(h(),b()),a()))) Ground Confluence Processor: UNC by decision procedure.