EFA is theory of arithmetic.
For a number $l$, we define $EB(l)$ as the largest $n$ such that there is a predicate $\phi$ with $l$ or less symbols such that $EFA \vdash \forall x. \phi(x) \iff x = n$, where $n$ is inserted as a numeral. In other words, $EB$ is essentially the Rayo's function of EFA.
It is clear that $EB(n + 3) \ge n$, since we can define the predicate $\phi(x):x = n$ (where $n$ is represented as the successor function applied to $0$, $n$ times).
In fact, $EB$ grows at least as quickly as stacked exponential functions asymptotically, since we can do $\phi(x):x=\exp(2,\exp(2,\exp(2,\dots0))\dots)$.
So, what is the growth rate of $EB$?