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