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