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