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