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