2.10/1.35	NO
2.10/1.35	
2.10/1.35	Proof:
2.10/1.35	This system is not confluent.
2.10/1.35	Inlined conditions in System R.
2.10/1.35	For the unconditional CP nil = cons(z, ssp'(y, sub(0, z))) ctcap(nil) and ctcap(cons(z, ssp'(y, sub(0, z)))) wrt R_u are not unifiable.
2.10/1.35	
2.21/1.43	EOF