Problem: f(a()) -> c() b() -> c() b() -> a() Proof: Uncurry Processor: f4(f(),a()) -> c() b() -> c() b() -> a() Ground Confluence Processor: not UNR by decision procedure.