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