Why k- Vertex Cover is not in PTIME when it can be expressed in FO-logic

Question

We can express property that graph has vertex cover of size at most k with first order formula:

$$\exists x_1 \exists x_2...\exists x_k (\forall y \forall z (E(z,y) \ \rightarrow \ \bigvee_{1 \leq i \leq k} y=x_i \ \vee \ \bigvee_{1 \leq i \leq k} z=x_i))$$

But, there is also theorem (proven for example in Libkin's book Finite model theory) that for every given FO sentence and finite model A one can decide does:

$$A \models \varphi$$

in PTIME.

Why can't we use this for sentence expressing k-VC property, written above, and decide does any given graph has this property?