NO

Problem:
 plus(x,0()) -> x
 plus(0(),1()) -> 1()
 plus(x,plus(y,1())) -> plus(plus(x,y),1())
 times(x,0()) -> 0()
 times(x,1()) -> x
 times(x,plus(y,1())) -> plus(times(x,y),x)
 m(0()) -> 0()
 plus(m(1()),1()) -> 0()
 plus(m(plus(x,1())),1()) -> m(x)
 m(m(x)) -> x
 plus(x,m(y)) -> m(plus(m(x),y))
 times(x,m(y)) -> m(times(x,y))

Proof:
 Nonconfluence Processor:
  terms: x *<- times(x,plus(0(),1())) ->* plus(0(),x)
  Qed