The formula is translated into the syntax of the normal form of lax-512892, over a vocabulary with one symbol for each relation symbol and a nullary symbol for falsum. Its normal form has radii at most $7^q − 1$ and at most $q + k$ witnesses in each basic local sentence. Every local formula in it has quantifier depth at most $q · (k + q + 2 + 6 · 7^q + 4α)$, a bound that depends on the arity $α$ of the vocabulary but not on its symbols. Back in mathlib's syntax, each ball-restricted quantifier gets a dist-formula guard of quantifier rank at most $7^q + α$, which gives the rank bound $p = q · (k + q + 2 + 6 · 7^q + 4α) + q + k + 2 · 7^q + 2α$.