NO
(ignored inputs)COMMENT reduction failed
Rewrite Rules:
   [ 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)) ]
Apply Direct Methods...
Inner CPs:
   [ plus(?x_1,1) = plus(plus(?x_1,0),1),
     plus(?x_1,0) = plus(plus(?x_1,m(1)),1),
     plus(?x_1,m(?x_5)) = plus(plus(?x_1,m(plus(?x_5,1))),1),
     times(?x_4,1) = plus(times(?x_4,0),?x_4),
     times(?x_4,0) = plus(times(?x_4,m(1)),?x_4),
     times(?x_4,m(?x_5)) = plus(times(?x_4,m(plus(?x_5,1))),?x_4),
     plus(m(1),1) = m(0),
     plus(m(0),1) = m(m(1)),
     m(0) = 0,
     plus(?x_7,0) = m(plus(m(?x_7),0)),
     plus(?x_7,?x_6) = m(plus(m(?x_7),m(?x_6))),
     times(?x_8,0) = m(times(?x_8,0)),
     times(?x_8,?x_6) = m(times(?x_8,m(?x_6))),
     plus(m(m(?x)),1) = m(m(plus(?x,1))),
     m(?x) = m(?x) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Combined result: not CR
/tmp/filefTdsIn.trs: Success(not CR)
(5 msec.)