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