1.99/1.30	NO
1.99/1.30	
1.99/1.30	Proof:
1.99/1.31	This system is not confluent.
1.99/1.31	For the unconditional CP t(k) = t(l) ctcap(t(k)) and ctcap(t(l)) wrt R_u are not unifiable.
1.99/1.31	
1.99/1.33	EOF