NO Problem: f(g(f(x))) -> x f(g(x)) -> g(f(x)) Proof: Nonconfluence Processor: terms: g(f(f(f4()))) *<- f(g(f(f4()))) ->* f4() Qed first automaton: final states: {8} transitions: f(10) -> 11* f(9) -> 10* g(11) -> 8* f4() -> 9* second automaton: final states: {12} transitions: f4() -> 12*