Problem: f(f(x,y),z) -> f(x,f(y,z)) f(i(x1),x1) -> e() Proof: Nonconfluence Processor: terms: f(e(),f(y,z)) *<- f(f(f(i(x39),x39),y),z) ->* f(i(x39),f(x39,f(y,z))) Qed