As far as I can tell, for any $\Pi_2$ theorem of Robinson arithmetic
$\forall_{x_1,\dots,x_m} \exists_{y_1,\dots,y_n} P(x_1,\dots,x_m,y_1,\dots,y_n)$
where $P$ is quantifier-free, there is a subexponential-time algorithm to find $y_1,\dots,y_n$ given $x_1,\dots,x_m$. A counterexample would be the sentence $\forall_x \exists_y (2^x = y)$, expressed using the $\beta$ function — since the size of the output is exponential in the size of the input it can't be computed by a subexponential-time ($x^{o(1)}$) algorithm. But I understand it's not a theorem since Robinson arithmetic can't prove $2^x$ is total, that would require induction.
Is this true? Or can Robinson arithmetic prove sentences whose satisfying values can't be found in subexponential time?