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