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