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