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