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