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