1.09/0.76	NO
1.09/0.76	
1.09/0.76	Proof:
1.09/0.77	This system is not confluent.
1.09/0.77	For the unconditional CP s(b) = t(b) ctcap(s(b)) and ctcap(t(b)) wrt R_u are not unifiable.
1.09/0.77	
1.24/0.78	EOF