Problem: h(f(),a(),a()) -> h(g(),a(),a()) h(g(),a(),a()) -> h(f(),a(),a()) a() -> a'() h(x,a'(),y) -> h(x,y,y) h(x,y,a'()) -> h(x,y,y) Proof: Nonconfluence Processor: terms: h(f(),a'(),a'()) *<- h(f(),a(),a()) ->* h(g(),a'(),a'()) Qed