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