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