1.92/1.23	YES
1.92/1.23	
1.92/1.23	Proof:
1.92/1.23	This system is confluent.
1.92/1.23	Removed infeasible rules from system R.
1.92/1.23	By \cite{GNG13}, Theorem 9.
1.92/1.23	This system is of type 3 or smaller.
1.92/1.23	This system is deterministic.
1.92/1.23	This system is weakly left-linear.
1.92/1.23	System R transformed to optimized U(R).
1.92/1.23	This system is orthogonal.
1.92/1.23	
1.97/1.27	EOF