2.29/1.43	YES
2.29/1.43	proof: 
2.29/1.43	  Conditions are infeasible.
2.29/1.43	  There are some non-trivial conditions.
2.29/1.43	  '\Sigma(e(x1)) \cap (->^*_R^_1)[\Sigma(REN(true))]' is empty by ETAC.
2.49/1.46	EOF