NO Problem: f(a(),b(),x) -> f(x,x,x) a() -> c() Proof: Nonconfluence Processor: terms: f(c(),b(),f4()) *<- f(a(),b(),f4()) ->* f(f4(),f4(),f4()) Qed first automaton: final states: {1} transitions: c() -> 4* b() -> 3* f4() -> 2* f(4,3,2) -> 1* second automaton: final states: {5} transitions: f4() -> 8,7,6 f(8,7,6) -> 5*