NO Problem: c() -> h(a(),h(f(f(f(f(c())))),h(a(),h(b(),b())))) h(h(c(),f(f(a()))),f(b())) -> a() h(c(),f(f(c()))) -> f(f(a())) h(f(h(c(),b())),h(h(h(b(),a()),h(c(),f(h(h(b(),a()),a())))),c())) -> c() Proof: Nonconfluence Processor: terms: h(h(h(a(),h(f(f(f(f(c())))),h(a(),h(b(),b())))),f(f(a()))),f(b())) *<- h(h(c(),f(f(a()))),f(b())) ->* a() Qed