Recall that a group $G$ is pseudofinite if every first-order sentence $\varphi$ (in the language of groups) satisfied in $G$ is also satisfied in some finite group. Also recall that an instance of the order property in $G$ is a pair of sequences of finite tuples of elements of $G$, $\{\bar{a}_i\}_{i<\omega}$ and $\{\bar{b}_{j}\}_{j < \omega}$ (with any two $\bar{a}_i$'s the same length and any two $\bar{b}_{j}$'s the same length), together with a formula $\varphi(\bar{x},\bar{y})$ such that for any $i, j < \omega$, $G$ satisfies $\varphi(\bar{a}_i,\bar{b}_j)$ if and only if $i<j$.
I'm curious about the existence of such a thing with $\varphi$ a quantifier free formula. Using some typical arguments, you can show that if such a thing exists, then it exists with $\varphi$ a positive atomic formula, which can further be reduced to an expression of the form $t(\bar{x},\bar{y})=e$, with $e$ the group identity. By rearranging the tuples in question and possibly adding inverses and instances of $e$ in, we can actually assuming that this expression is of the form $\prod_{\ell<n} x_\ell y_\ell = e$. By a compactness argument, this finally reduces to the following question:
Question: Does there exist an $n< \omega$ such that for every $k< \omega$, there is a finite group $H$ together with $n$-tuples $\bar{a}^0,\dots,\bar{a}^{k-1},\bar{b}^0,\dots,\bar{b}^{k-1} \in H$ for which for any $i,j < k$, $\prod_{\ell<n} a^i_\ell b^j_\ell = e$ if and only if $i < j$?
This is pretty likely to be true and also likely to be known, but I'm having difficulty thinking of something or finding a reference. I'm also curious about quantifier-free instances of the independence property and the strong order property, but I wanted to keep this question focused.