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