<= 0 =>

Notice that the applicable rule is existential and will introduce a Skolem constant.