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