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