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