NO Problem: a() -> h(a()) a() -> f(c()) f(x) -> h(g(x)) h(x) -> f(g(x)) Proof: Nonconfluence Processor: terms: f(c()) *<- a() ->* h(f(c())) Qed first automaton: final states: {1} transitions: h(57) -> 1* c() -> 2* f(2) -> 1* g(57) -> 2* g(2) -> 57* second automaton: final states: {8} transitions: h(55) -> 10* h(10) -> 8* c() -> 9* f(142) -> 8* f(9) -> 10* g(55) -> 9* g(10) -> 142* g(142) -> 10* g(9) -> 55*