2.08/1.35 NO 2.08/1.35 2.08/1.36 Proof: 2.08/1.36 This system is not confluent. 2.08/1.36 For the unconditional CP tp2(z, x') = tp2(0, add(z, x')) the left- and right-hand sides are two different normal forms wrt R_u. 2.08/1.36 2.08/1.38 EOF