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