Problem: a() -> a() g(g(a())) -> b() g(g(x)) -> g(g(g(b()))) Proof: Nonconfluence Processor: terms: b() *<- g(g(a())) ->* g(g(g(b()))) Qed first automaton: final states: {10} transitions: b() -> 10* second automaton: final states: {6} transitions: g(8) -> 9* g(9) -> 9,6 g(7) -> 8* b() -> 7*