0.00/0.01	YES
0.00/0.01	
0.00/0.01	1 decompositions
0.00/0.01	 #0 -----------
0.00/0.01	   1: +(0(),x1) -> x1
0.00/0.01	   2: +(s(0()),x2) -> s(x2)
0.00/0.01	   3: s(s(x3)) -> x3
0.00/0.01	
0.00/0.01	@Jouannaud and Kirchner's criterion
0.00/0.01	--- R
0.00/0.01	   1: +(0(),x1) -> x1
0.00/0.01	   2: +(s(0()),x2) -> s(x2)
0.00/0.01	   3: s(s(x3)) -> x3
0.00/0.01	
0.00/0.01	--- S
0.00/0.01	   1: +(0(),x1) -> x1
0.00/0.01	   2: +(s(0()),x2) -> s(x2)
0.00/0.01	   3: s(s(x3)) -> x3
0.00/0.01	
0.00/0.01	
0.00/0.01	EOF