For any two non-isomorphic graphs $G, H$, does there exist a polysize, polylog quantifier depth first order formula which witnesses this?
Thanks to my colleague Maxim Zhukovskii for suggesting this answer.

It turns out that the answer is negative, and the counterexample is rather simple. Just take $G=K_m\sqcup \overline{K_m}$ and $H=K_{m+1}\sqcup \overline{K_{m-1}}$ for $n=2m$ and $G=K_m\sqcup \overline{K_{m+1}}$ and $H=K_{m+1}\sqcup \overline{K_m}$ for $n=2m+1$. (Here $K_s$ is an $s$-clique and $\overline{K_s}$ is a set of $s$ isolated vertices). By considering the Ehrenfeucht game one can show that in the first case the minimal possible depth is $m$ and in the second case it is $m+1$.

It was shown in the paper "The first order definability of graphs: Upper bounds for quantifier depth" by Oleg Pikhurko, Helmut Veith and Oleg Verbitsky that this bound is almost tight and any two $n$-vertex graphs are distinguishable by a formula of depth $\frac{n+3}{2}$.