In Game-Theoretic Semantics (Hintikka games) for First-Order Logic, a game is played on a formula between Eloise (who tries to show the formula is True) and Abelard (who tries to show the formula is False). Consider the sentence $\phi = \forall x \in \mathbb{Z} \exists y \in \mathbb{Z} (y^2 - x^2 = 3)$. Which player has a winning strategy, and what is their winning move?