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