4.12/4.15	YES
4.12/4.15	
4.12/4.15	1 decompositions
4.12/4.15	 #0 -----------
4.12/4.15	   1: +(+(x,y),z) -> +(x,+(y,z))
4.12/4.15	   2: +(x,y) -> +(y,x)
4.12/4.15	   3: *(*(x,y),z) -> *(x,*(y,z))
4.12/4.15	   4: *(x,y) -> *(y,x)
4.12/4.15	   5: *(+(x,y),z) -> +(*(x,z),*(y,z))
4.12/4.15	   6: *(x,+(y,z)) -> +(*(x,y),*(x,z))
4.12/4.15	
4.12/4.15	@Jouannaud and Kirchner's criterion
4.12/4.15	--- R
4.12/4.15	   1: +(+(x,y),z) -> +(x,+(y,z))
4.12/4.15	   2: +(x,y) -> +(y,x)
4.12/4.15	   3: *(*(x,y),z) -> *(x,*(y,z))
4.12/4.15	   4: *(x,y) -> *(y,x)
4.12/4.15	   5: *(+(x,y),z) -> +(*(x,z),*(y,z))
4.12/4.15	   6: *(x,+(y,z)) -> +(*(x,y),*(x,z))
4.12/4.15	
4.12/4.15	--- S
4.12/4.15	   1: +(+(x,y),z) -> +(x,+(y,z))
4.12/4.15	   2: +(x,y) -> +(y,x)
4.12/4.15	   3: *(*(x,y),z) -> *(x,*(y,z))
4.12/4.15	   4: *(x,y) -> *(y,x)
4.12/4.15	   5: *(+(x,y),z) -> +(*(x,z),*(y,z))
4.12/4.15	   6: *(x,+(y,z)) -> +(*(x,y),*(x,z))
4.12/4.15	
4.12/4.15	
4.12/4.15	EOF