NO
(ignored inputs)COMMENT experiments for [36] submitted by: Takahito Aoto
input TRS:
   [ br(0,?y,?z) -> ?y,
     br(s(?x),?y,?z) -> ?z,
     p(0) -> 0,
     p(s(?x)) -> ?x,
     +(?x,?y) -> br(?x,?y,+(p(?x),s(?y))),
     +(?x,?y) -> br(?y,?x,+(s(?x),p(?y))) ]
TRS:
   [ br(0,?y,?z) -> ?y,
     br(s(?x),?y,?z) -> ?z,
     p(0) -> 0,
     p(s(?x)) -> ?x,
     +(?x,?y) -> br(?x,?y,+(p(?x),s(?y))),
     +(?x,?y) -> br(?y,?x,+(s(?x),p(?y))) ]
Check distinct normal forms in critical pair closure
convertible distinct normal forms: br(?x,0,s(p(?x))) = ?x
problems/584.trs: Success(not UNC)
(8 msec.)