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