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