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