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