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