Problem: a() -> a() a() -> g(a()) g(g(b())) -> a() g(g(b())) -> b() Proof: Uncurry Processor: a() -> a() a() -> f3(g(),a()) f3(g(),f3(g(),b())) -> a() f3(g(),f3(g(),b())) -> b() Ground Confluence Processor: UN by decision procedure.