2.74/1.17	YES
2.74/1.17	
2.74/1.17	Proof:
2.74/1.17	This system is confluent.
2.74/1.17	By \cite{SMI95}, Corollary 4.7 or 5.3.
2.74/1.17	This system is oriented.
2.74/1.17	This system is of type 3 or smaller.
2.74/1.17	This system is right-stable.
2.74/1.17	This system is properly oriented.
2.74/1.17	This is an overlay system.
2.74/1.17	This system is left-linear.
2.74/1.17	All 2 critical pairs are trivial or infeasible.
2.74/1.17	Overlap: (rule1: g(y) -> a <= h(y) = b, rule2: g(z) -> z, pos: ε, mgu: {(z,y)})
2.74/1.17	CP: y = a <= h(y) = b
2.74/1.17	This critical pair is infeasible.
2.74/1.17	This critical pair is conditional.
2.74/1.17	This critical pair has some non-trivial conditions.
2.74/1.17	'\Sigma(h(y)) \cap (->^*_R)[\Sigma(REN(b))]' is empty.
2.74/1.17	Overlap: (rule1: g(y) -> y, rule2: g(z) -> a <= h(z) = b, pos: ε, mgu: {(z,y)})
2.74/1.17	CP: a = y <= h(y) = b
2.74/1.17	This critical pair is infeasible.
2.74/1.17	This critical pair is conditional.
2.74/1.17	This critical pair has some non-trivial conditions.
2.74/1.17	'\Sigma(h(y)) \cap (->^*_R)[\Sigma(REN(b))]' is empty.
2.74/1.17	
3.19/1.39	EOF