Problem: f(f(x,y),z) -> f(x,f(y,z)) f(x,1()) -> x Proof: Nonconfluence Processor: terms: f(x31,f(y,z)) *<- f(f(f(x31,1()),y),z) ->* f(x31,f(1(),f(y,z))) Qed