6.80/2.71	YES
6.80/2.71	
6.80/2.71	Proof:
6.80/2.72	This system is confluent.
6.80/2.72	By \cite{GNG13}, Theorem 9.
6.80/2.72	This system is of type 3 or smaller.
6.80/2.72	This system is deterministic.
6.80/2.72	This system is weakly left-linear.
6.80/2.72	System R transformed to optimized U(R).
6.80/2.72	This system is orthogonal.
6.80/2.72	
9.13/3.28	EOF