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