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