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