0.00/0.03	NO
0.00/0.03	(ignored inputs)COMMENT COPS 585 586 COMMENT submitted by: Kiraku Shintani
0.00/0.03	Rewrite Rules (1):
0.00/0.03	   [ +(0,?y) -> ?y,
0.00/0.03	     +(s(?x),?y) -> s(+(?x,?y)),
0.00/0.03	     s(s(?x)) -> ?x ]
0.00/0.03	Rewrite Rules (2):
0.00/0.03	   [ +(0,?y) -> ?y,
0.00/0.03	     +(s(0),?y) -> s(?y),
0.00/0.03	     +(s(s(?x)),?y) -> s(s(+(?y,?x))) ]
0.00/0.03	both left-linear
0.00/0.03	check commutation with R1 := (1), R2 := (2)
0.00/0.03	check CPs are development closed...
0.00/0.03	...failed
0.00/0.03	check commutation with R1 := (2), R2 := (1)
0.00/0.03	check CPs are development closed...
0.00/0.03	...failed
0.00/0.03	check non-commutation
0.00/0.03	check with R1 := (1), R2 := (2)
0.00/0.03	check counter example from CPs...
0.00/0.03	check candidate: <?y, ?y>
0.00/0.03	check candidate: <s(?y), s(+(0,?y))>
0.00/0.03	check candidate: <s(s(+(?y,?x))), s(+(s(?x),?y))>
0.00/0.03	Counter example: s(s(+(?y,?x))) <-R2- +(s(s(?x)),?y) -R1-> s(+(s(?x),?y))
0.00/0.03	
0.00/0.03	result: not COM
0.00/0.03	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(not COM)
0.00/0.03	(0 msec.)
0.00/0.03	EOF