2.24/1.42	NO
2.24/1.42	
2.24/1.42	Proof:
2.24/1.42	This system is not confluent.
2.24/1.42	Removed infeasible rules from system R.
2.24/1.42	For the unconditional CP gcd(z', s(add(y', z'))) = gcd(s(y'), z') the left- and right-hand sides are two different normal forms wrt R_u.
2.24/1.42	
3.79/2.05	EOF