NO Problem: c() -> f(c()) c() -> f(h(a())) f(x) -> h(f(x)) Proof: Nonconfluence Processor: terms: h(f(h(a()))) *<- c() ->* f(f(h(a()))) Qed first automaton: final states: {1} transitions: h(4) -> 4,1 h(2) -> 3* f(3) -> 4* a() -> 2* second automaton: final states: {8} transitions: h(11) -> 11* h(8) -> 8* h(9) -> 10* f(11) -> 8* f(10) -> 11* a() -> 9*