NO Problem: c() -> f(f(c())) h(h(h(b(),b()),f(f(a()))),f(f(f(a())))) -> a() b() -> h(h(f(a()),c()),f(a())) Proof: Nonconfluence Processor: terms: h(h(h(b(),h(h(f(a()),c()),f(a()))),f(f(a()))),f(f(f(a())))) *<- h(h(h(b(),b()),f(f(a()))),f(f(f(a())))) ->* a() Qed first automaton: final states: {1} transitions: h(17,8) -> 18* h(14,10) -> 15* h(16,15) -> 17* h(14,3) -> 16* h(13,11) -> 14* h(18,5) -> 1* c() -> 11* f(12) -> 13* f(9) -> 10* f(4) -> 5* f(7) -> 8* f(11) -> 48* f(6) -> 7* f(3) -> 4* f(2) -> 3* f(48) -> 11* a() -> 12,9,6,2 b() -> 16* second automaton: final states: {19} transitions: a() -> 19*