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