2.10/1.31 NO 2.10/1.31 2.10/1.31 Proof: 2.10/1.31 This system is not confluent. 2.10/1.31 For the unconditional CP c = d ctcap(c) and ctcap(d) wrt R_u are not unifiable. 2.10/1.31 2.10/1.33 EOF