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