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