2.32/1.39	NO
2.32/1.39	
2.32/1.39	Proof:
2.32/1.39	This system is not confluent.
2.32/1.39	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.32/1.39	
3.36/1.83	EOF