Problem: a() -> a() a() -> g(a()) g(g(b())) -> a() g(g(b())) -> b() Proof: Nonconfluence Processor: terms: a() *<- g(g(b())) ->* b() Qed first automaton: final states: {2} transitions: a() -> 2* g(2) -> 2* second automaton: final states: {1} transitions: b() -> 1*