NO
(ignored inputs)COMMENT experiments for [125] submitted by: Takahito Aoto
input TRS:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> +(?x,p(?y)),
     p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> p(s(?x)),
     p(s(0)) -> 0 ]
TRS:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> +(?x,p(?y)),
     p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> p(s(?x)),
     p(s(0)) -> 0 ]
constructed TRS:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> +(?x,p(?y)),
     p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> p(s(?x)),
     p(s(0)) -> 0,
     +(p(s(?x_4)),?y_1) -> s(+(?x_4,p(?y_1))),
     +(s(p(?x_3)),?y_2) -> s(+(?x_3,p(?y_2))),
     +(s(0),p(?y_2)) -> ?y_2,
     s(p(0)) -> 0,
     p(s(s(0))) -> s(0),
     s(+(0,p(?y_11))) -> ?y_11,
     s(+(p(0),?y_1)) -> ?y_1,
     +(s(s(0)),p(?y_2)) -> +(s(0),?y_2),
     s(p(p(0))) -> p(0),
     p(s(s(s(0)))) -> s(s(0)),
     +(p(p(s(?x_4))),?y_5) -> s(+(?x_4,p(p(?y_5)))),
     s(+(p(0),p(?y_5))) -> +(p(0),?y_5),
     +(s(0),?y_5) -> s(?y_5),
     +(s(s(p(?x_3))),?y_9) -> s(s(+(?x_3,p(?y_9)))),
     s(+(s(s(0)),p(?y_9))) -> +(s(s(0)),?y_9),
     +(s(0),s(p(?x_3))) -> s(?x_3),
     +(s(0),0) -> s(0),
     +(s(0),s(0)) -> s(s(0)),
     s(+(+(0,p(?y_12)),?y_1)) -> +(?y_12,?y_1),
     s(+(+(p(0),?y_13),?y_1)) -> +(?y_13,?y_1),
     s(+(p(p(0)),?y_1)) -> +(p(0),?y_1),
     s(+(+(p(0),p(?y_17)),?y_1)) -> +(+(p(0),?y_17),?y_1),
     +(+(s(s(0)),?y_26),?y_1) -> s(+(+(s(0),?y_26),?y_1)),
     s(+(0,s(p(?x_27)))) -> s(?x_27),
     +(s(s(s(0))),p(?y_2)) -> +(s(s(0)),?y_2),
     s(p(+(0,p(?y_12)))) -> p(?y_12),
     s(p(+(p(0),?y_13))) -> p(?y_13),
     s(p(p(p(0)))) -> p(p(0)),
     s(p(+(p(0),p(?y_17)))) -> p(+(p(0),?y_17)),
     p(+(s(s(0)),?y_26)) -> s(p(+(s(0),?y_26))),
     p(s(s(s(s(0))))) -> s(s(s(0))),
     s(+(+(0,p(?y_12)),p(?y_5))) -> +(?y_12,p(?y_5)),
     s(+(+(p(0),?y_13),p(?y_5))) -> +(?y_13,p(?y_5)),
     s(+(p(p(0)),p(?y_5))) -> +(p(p(0)),?y_5),
     s(+(+(p(0),p(?y_17)),p(?y_5))) -> +(p(+(p(0),?y_17)),?y_5),
     +(p(+(s(s(0)),?y_26)),?y_5) -> s(+(+(s(0),?y_26),p(?y_5))),
     s(+(s(s(s(0))),p(?y_9))) -> +(s(s(s(0))),?y_9),
     s(p(?y_11)) -> ?y_11,
     +(p(0),?y_17) -> p(?y_17),
     +(s(s(0)),s(p(?x_3))) -> s(s(?x_3)),
     +(s(s(0)),0) -> s(s(0)),
     +(s(s(0)),s(0)) -> s(s(s(0))),
     +(s(s(0)),s(s(0))) -> s(s(s(s(0)))),
     +(p(s(p(?x_3))),?y_16) -> s(+(?x_3,p(p(?y_16)))),
     +(p(p(p(s(?x_4)))),?y_16) -> s(+(?x_4,p(p(p(?y_16))))),
     +(p(s(0)),?y_16) -> s(p(?y_16)),
     s(+(+(0,p(?y_12)),p(p(?y_16)))) -> +(p(p(?y_12)),?y_16),
     s(+(+(p(0),?y_13),p(p(?y_16)))) -> +(p(p(?y_13)),?y_16),
     s(+(p(p(0)),p(p(?y_16)))) -> +(p(p(p(0))),?y_16),
     s(+(+(p(0),p(?y_17)),p(p(?y_16)))) -> +(p(p(+(p(0),?y_17))),?y_16),
     +(p(p(+(s(s(0)),?y_26))),?y_16) -> s(+(+(s(0),?y_26),p(p(?y_16)))),
     +(p(0),s(?x_3)) -> s(p(?x_3)),
     +(p(0),s(0)) -> 0,
     +(p(0),s(s(0))) -> s(0),
     +(p(0),s(s(s(0)))) -> s(s(0)),
     s(s(p(?x_27))) -> s(?x_27),
     +(s(s(s(p(?x_3)))),?y_25) -> s(s(s(+(?x_3,p(?y_25))))),
     +(s(p(s(?x_4))),?y_25) -> s(s(+(?x_4,p(?y_25)))),
     +(s(s(0)),?y_25) -> s(s(?y_25)),
     s(s(+(s(s(s(0))),p(?y_25)))) -> +(s(s(s(s(0)))),?y_25),
     s(+(s(s(0)),s(p(?x_3)))) -> +(s(s(0)),s(?x_3)),
     s(+(s(s(0)),0)) -> +(s(s(0)),s(0)),
     s(+(s(s(0)),s(0))) -> +(s(s(0)),s(s(0))),
     s(+(s(s(0)),s(s(0)))) -> +(s(s(0)),s(s(s(0)))),
     +(s(0),s(s(p(?x_3)))) -> s(s(?x_3)) ]
convertible distinct normal forms: +(?y_157,?y_257) = s(s(+(?y_157,p(p(?y_257)))))
UNC Completion (Strongly Closed)
problems/614.trs: Success(not UNC)
(436 msec.)