NO Problem: b() -> f(b()) f(a()) -> f(h(h(h(h(c(),b()),a()),f(c())),c())) c() -> h(f(c()),f(h(c(),a()))) c() -> f(b()) Proof: Nonconfluence Processor: terms: h(f(c()),f(h(c(),a()))) *<- c() ->* f(b()) Qed first automaton: final states: {3} transitions: c() -> 8,5 b() -> 48* f(8) -> 9* f(6) -> 7* f(48) -> 48,5,8 h(5,4) -> 6* h(9,7) -> 5,8,3 a() -> 4* second automaton: final states: {1} transitions: b() -> 2* f(2) -> 2,1