Problem: b() -> a() f(h(b(),f(a()))) -> f(c()) c() -> h(c(),c()) h(f(f(b())),a()) -> c() h(a(),a()) -> a() Proof: Nonconfluence Processor: terms: f(h(a(),f(a()))) *<- f(h(b(),f(a()))) ->* f(c()) Qed first automaton: final states: {7} transitions: h(10,9) -> 11* a() -> 10,8 f(11) -> 7* f(8) -> 9* second automaton: final states: {12} transitions: h(13,13) -> 13* c() -> 13* f(13) -> 12*