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