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