YES Problem: f(a()) -> b() f(a()) -> f(c()) a() -> d() f(d()) -> b() f(c()) -> b() d() -> c() Proof: Uncurry Processor: f5(f(),a()) -> b() f5(f(),a()) -> f5(f(),c()) a() -> d() f5(f(),d()) -> b() f5(f(),c()) -> b() d() -> c() Ground Confluence Processor: confluent by decision procedure.