3.81/1.83	NO
3.81/1.83	
3.81/1.83	Proof:
3.81/1.83	This system is not confluent.
3.81/1.83	Inlined conditions in System R.
3.81/1.83	For the unconditional CP ssp($1, y') = cons(z', ssp($1, sub(y', z'))) the left- and right-hand sides are two different normal forms wrt R_u.
3.81/1.83	
5.45/2.22	EOF