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