I will show how to improve Tulipani’s construction from $O(p^5)$ symbols to $O(p^3)$ symbols, or $O(p^3\log p)$ bits.
Recall that Tulipani’s sentence is
$$H_p=\forall\vec x\,\exists\vec s\,\exists\vec u\,\exists y\:\Bigl(G_p(\vec x,\vec s,\vec u)\land\let\ET\bigwedge\ET_i(y=x_i\land u_p=x_0\to x_1=x_0)\Bigr),$$
where $G_p(\vec x,\vec s,\vec u)$ is a Horn formula in variables $\{x_i:0\le i<p\}$, $\{s_{ij}:0\le i\le j<p\}$, $\{u_i:2\le i\le p\}$, defined as the conjunction of
$$\begin{gather}
\tag1\label{assoc}\ET_{i,j,k,h,r}(x_h=s'_{ij}\land x_r=s'_{jk}\to s'_{hk}=s'_{ir}),\\
\tag2\label{canc}\ET_{i,j,k}(s'_{ij}=s'_{ik}\to x_j=x_k),\\
\tag3\label{zero}\ET_is_{0i}=x_i,\\
\tag4\label{cyc}u_2=s_{11}\land\ET_{2\le j<p}\ET_i(u_j=x_i\to u_{j+1}=s'_{1i}),
\end{gather}$$
where $s'_{ij}:=s_{\min\{i,j\},\max\{i,j\}}$. The meaning of $G_p$ is that given elements $\vec a,\vec b,\vec c$ of a model such that each $b_{ij}$ belongs to the set $A=\{a_i:i<p\}$, $G_p(\vec a,\vec b,\vec c)$ is true iff the recipe
$$\tag+\label{add}a_i+a_j=a_j+a_i=b_{ij},\qquad i\le j<p,$$
gives a well-defined operation $+$ on $A$ such that
The bottleneck here is the formula $\eqref{assoc}$ with $p^5$ conjuncts, which ensures (in view of $\eqref{zero}$) that $+$ is well defined, and associative.
First, I claim that one can replace $\eqref{assoc}$ with the two formulas
$$\begin{gather}
\tag{$1'$}\label{def}\ET_{i,j,k}(x_i=x_j\to s'_{ik}=s'_{jk}),\\
\tag{$1''$}\label{nucl}\ET_{i,j,h,r}(x_h=s'_{ij}\land x_r=s'_{j1}\to s'_{h1}=s'_{ir})
\end{gather}$$
with $O(p^4)$ symbols. Let $G'_p$ denote $\eqref{def}\land\eqref{nucl}\land\eqref{canc}\land\eqref{zero}\land\eqref{cyc}$, and let $H'_p$ be $H_p$ with $G_p$ replaced with $G'_p$. It is easy to see that if $A=\{a_i:i<p\}$ and $\vec b\in A$, then $G'_p(\vec a,\vec b,\vec c)$ holds iff $\eqref{add}$ gives a well-defined operation on $A$ such that
$(A,+)$ is a commutative loop with zero element $a_0$,
$a_1$ belongs to the nucleus
$$N=\{z\in A:\forall x,y\in A\:(x+y)+z=x+(y+z)\},$$
$c_j=ja_1$ for each $j$ (meaning a sum of $j$ copies of $a_1$, whose bracketing does not matter because of the previous point).
Since $G_p$ implies $G'_p$, $H'_p$ still holds in models of size $\ne p$.
The nucleus $N$ is associative, and it is a subgroup of $A$. If $\sim$ denotes the equivalence relation
$$a\sim b\iff N+a=N+b,$$
then the equivalence class of $a$ is $N+a$: on the one hand, if $a\sim b$, then $b\in N+b=N+a$ as $0\in N$. On the other hand, if $b=n+a$ with $n\in N$, then
$$N+b=N+(n+a)=(N+n)+a=N+a$$
using the definition of $N$ and the fact that it is a subgroup. Thus,
$$\{N+a:a\in A\}$$
is a partition of $A$ into sets of size $|N+a|=|N|$. As a consequence, $|N|$ divides $|A|$, and more generally, if $H$ is a subgroup of $N$, then $|H|$ divides $|A|$.
In particular, if $G'_p(\vec a,\vec b,\vec c)$ where the $a_i$ are pairwise distinct, then the order of the cyclic subgroup of $A$ generated by $a_1$ divides $p=|A|$. This implies that $H'_p$ fails in a model of size $p$ if we take for $\vec x$ a bijective enumeration of its elements, using the same argument as Tulipani.
This gives a sentence $H'_p$ with $O(p^4)$ symbols. In order to further reduce it to $O(p^3)$, note that $\eqref{nucl}$ can be replaced with
$$\ET_{i,j}\exists z\ET_h\bigl((x_h=s'_{ij}\to s'_{h1}=z)\land(x_h=s'_{j1}\to s'_{ih}=z)\bigr).$$
If we want to keep $H'_p$ in prenex normal form, we can introduce new variables $\{z_{ij}:i,j<p\}$, expand the quantifier prefix of $H'_p$ to $\forall\vec x\,\exists\vec s\,\exists\vec u\,\exists y\,\exists\vec z$, and replace $\eqref{nucl}$ with
$$\ET_{i,j,h}\bigl((x_h=s'_{ij}\to s'_{h1}=z_{ij})\land(x_h=s'_{j1}\to s'_{ih}=z_{ij})\bigr).$$
This gives a sentence with $O(p^3)$ symbols, still using $O(p^2)$ variables.
A few more optimizations, which however do not change the $O(p^3)$ asymptotic:
We can drop $\eqref{def}$. On the one hand, this only makes the sentence weaker, hence it continues to hold in models of size $\ne p$. On the other hand, the failure for models of size $p$ is achieved when the $x_i$ are pairwise distinct, in which case $\eqref{def}$ holds automatically.
We can drop $\eqref{zero}$ and the $s_{0i}$ variables, putting $s'_{0i}:=x_i$ instead.
We only use the $u_j$ variables to compute $u_p=px_1$. If we count to $p$ using doubling rather than adding $1$ at each step, we only need the $O(\log p)$ variables $u_j$ for $j=\lfloor p2^{-k}\rfloor$, $k\le\log_2p-2$, and we can reduce the size of $\eqref{cyc}$ to $O(p\log p)$ symbols.
It’s hard to guess what the optimal size should be; the only lower bound I can think of is that using a straightforward pebble game argument, any sentence (Horn or otherwise) that distinguishes a set with $p$ elements from a set with $p+1$ elements needs to use more than $p$ distinct variables (and a fortiori needs quantifier rank more than $p$). This bound is tight for not-necessarily-Horn sentences, as exhibited in the question.
