The bounded temporal expansion converts eventually into an existential quantification, which will often be skolemized; alternative solutions will be returned depending on the value of that skolemized value, but in the perspective of the user, these all represent the same temporal instance (since temporal expansion is opaque).