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