At the request of the OP, I’m writing a lengthy nonanswer showing that there are short proofs of inconsistency of similar theories where the “big number” is given by a term in the usual language of arithmetic $L_{PA}=\{0,S,+,\cdot\}$, possibly expanded by the exponential function. The argument does not work for languages including faster growing functions such as tetration, let alone the Ackermann function needed to succinctly represent the Graham number.
Let $|t|$ denote the size (= number of symbols) of a syntactic object $t$ (a term, a formula, etc.).
Theorem 1: For any closed $L_{PA}$-term $t$, there is a proof of $t\nless t$ in $Q$ (and therefore a proof of inconsistency in $Q+\forall x\,x<t$) with $O(|t|)$ lines, each of size $O(|t|)$.
Proof: We will use the fact that there are $Q$-definable cuts that interpret fragments of arithmetic such as $I\Delta_0$, see [1,§V.5(c)]. Specifically, there exists a formula $I(x)$ such that $Q$ proves
$$\begin{align}
&I(0),\\
&\forall x\,\forall y\:\bigl(I(x)\land I(y)\to I(S(x))\land I(x+y)\land I(x\cdot y)\bigr),\\
&\forall x\,\forall y\:\bigl(I(x)\land y<x\to I(y)\bigr),\\
&\forall x\:\bigl(I(x)\to x\nless x\bigr).
\end{align}$$
Let us fix $I$ and a $Q$-proof of the above. Then we prove
$$I(t)$$
by (meta)induction on the complexity of a closed term $t$: if, say $t$ is $t_0+t_1$, we instantiate one of the formulas above to obtain
$$I(t_0)\land I(t_1)\to I(t_0+t_1),$$
and we conclude $I(t_0+t_1)$ using the induction hypothesis and modus ponens. This argument involves $O(1)$ proof lines for each subterm of $t$, where each line has size $O(|t|)$. QED
In fact, the same argument shows more: since every $\Pi_1$ sentence $\psi$ provable in $I\Delta_0+\exp$ is interpretable on a cut in $Q$ by [1,Thm. V.5.26], we can take the cut $I$ above to satisfy $\psi$, and obtain
Theorem 2: Let $\theta(x)$ be a fixed $\Delta_0$ formula such that $I\Delta_0+\exp\vdash\forall x\,\theta(x)$. Then given a closed $L_{PA}$ term $t$, we can construct a $Q$-proof of $\theta(t)$ with $O(|t|)$ lines, each of size $O(|t|)$.
In order to adapt the argument to exponentiation, we need more work, as there are no definable cuts in $Q$ closed under exponentiation. Let $Q(\exp)$ be the theory in language $L_{\exp}=L_{PA}\cup\{x^y\}$ axiomatized by $Q$ and
$$\begin{align}
x^0&=1,\\
x^{S(y)}&=x^y\cdot x.
\end{align}$$
Theorem 3: Let $\theta(x)$ be a fixed $\Delta_0$ formula such that $I\Delta_0+\exp\vdash\forall x\,\theta(x)$. Then given a closed $L_{\exp}$ term $t$, we can construct a $Q(\exp)$-proof of $\theta(t)$ with $O(|t|)$ lines, each of size $O(|t|)$.
In particular, we can construct a proof of inconsistency in $Q(\exp)+\forall x\,x<t$ with such parameters.
Proof: As above, we fix a definable cut $I_0(x)$ that, provably in $Q(\exp)$, is closed under $+$ and $\cdot$, and satisfies $\mathrm{PA}^-$ and $\forall x\,\bigl(I_0(x)\to\theta(x)\bigr)$. Moreover, we can make sure $Q(\exp)$ proves
$$\begin{align}
\forall x\,\forall y\,\forall z\:\bigl(I_0(x)\land I_0(y)\land I_0(z)\to x^{y+z}&=x^y\cdot x^z\bigr),\\
\forall x\,\forall y\,\forall z\:\bigl(I_0(x)\land I_0(y)\land I_0(z)\to\:\, x^{y\cdot z}&=(x^y)^z\bigr).
\end{align}$$
We now define a sequence of shorter and shorter cuts by
$$I_{k+1}(x)\iff I_k(x)\land\forall y\:\bigl(I_k(y)\to I_k(y^x)\bigr).$$
Using the properties of $I_0$, it is easy to construct by metainduction on $k$ $Q(\exp)$ proofs that $I_k$ is a cut closed under $+$ and $\cdot$, using $O(1)$ proof lines for each $I_k$, i.e., $O(k)$ lines in total to prove the properties for $I_0,\dots,I_k$. Each line has size $O(|I_k|)$.
As defined, $I_{k+1}$ involves two occurrences of $I_k$, hence $|I_k|=O(2^k)$. Pretend for the moment that we can rewrite the definition of $I_{k+1}$ so that it only refers to $I_k$ once. Then $|I_k|=O(k)$, hence the proof so far has $O(k)$ lines, each of size $O(k)$.
$\DeclareMathOperator\ed{ed}$For any closed term $t$, we define the exponentiation nesting depth $\ed(t)$ by
$$\begin{align}
\ed(0)&=0,\\
\ed(S(t))&=\ed(t),\\
\ed(t\circ u)&=\max\{\ed(t),\ed(u)\},\qquad\circ\in\{+,\cdot\},\\
\ed(t^u)&=\max\{\ed(t),1+\ed(u)\}.
\end{align}$$
Then we construct $Q(\exp)$ proofs of
$$I_{k-\ed(t)}(t)$$
by induction on the complexity of a closed term $t$ such that $\ed(t)\le k$, using the properties of $I_0,\dots,I_k$ above. We use $O(1)$ proof lines for each $t$ on top of the induction hypothesis, hence $O(|t|+k)$ lines in total, each of size $O(|t|+k)$. Choosing $k=\ed(t)\le|t|$, we obtain a proof of
$$I_0(t),$$
and therefore of $\theta(t)$, with $O(|t|)$ lines, each of size $O(|t|)$.
It remains to show how to present the definition of $I_k$ so that it has size only $O(k)$. The basic idea is to use the equivalences
$$\begin{align}
\psi(x)\lor\psi(y)&\iff\exists z\:\bigl((z=x\lor z=y)\land\psi(z)\bigr),\\
\psi(x)\land\psi(y)&\iff\forall z\:\bigl((z=x\lor z=y)\to\psi(z)\bigr),
\end{align}$$
however, the definition of $I_{k+1}$ involves both a positive and a negative occurrence of $I_k$, and these cannot be contracted directly. To fix this, we encompass both polarities in a single predicate
$$J_k(x,a)\iff(a=0\land I_k(x))\lor(a\ne0\land\neg I_k(x)).$$
In order to make the notation manageable, let me write
$$\def\?{\mathrel?}(\phi\?\psi_0:\psi_1)\iff\bigl((\phi\land\psi_0)\lor(\neg\phi\land\psi_1)\bigr).$$
We can express $J_{k+1}$ in terms of $J_k$ as
$$\begin{align}
J_{k+1}(x,a)&\iff\bigl[a=0\?\forall y\,(J_k(y,1)\lor J_k(y^x,0)):\exists z\,(J_k(z,0)\land J_k(z^x,1))\bigr]\\
&\iff\begin{aligned}[t]
\bigl[a=0&\?\forall y\,\exists u,v\:\bigl((v=0\?u=y^x:u=y)\land J_k(u,v)\bigr)\\
&\,:\exists z\,(J_k(z,0)\land J_k(z^x,1))\bigr]
\end{aligned}\\
&\iff\begin{aligned}[t]
\forall y\,\exists z,u,v\:\bigl[a=0&\?(v=0\?u=y^x:u=y)\land J_k(u,v)\\
&\,:J_k(z,0)\land J_k(z^x,1)\bigr]
\end{aligned}\\
&\iff\forall y\,\exists z,u,v\:\bigl[\bigl(a=0\to(v=0\?u=y^x:u=y)\bigr)\\\
&\qquad\qquad{}\land\forall u',v'\:\bigl[\bigl(a=0\?u'=u\land v'=v:(v'=0\?u'=z:u'=z^x)\bigr)\\
&\qquad\qquad\qquad\qquad\qquad\qquad\qquad\to J_k(u',v')\bigr]\bigr].
\end{align}$$
Notice that even though the last expression looks complicated, it contains only one occurrence of $J_k$ (even if we expand the abbreviations), hence we use it as the definition of $J_{k+1}$. This way, we define formulas $J_k$ of size $O(k)$, and we put $I_k(x)\iff J_k(x,0)$.
Let me point out that a general method how to eliminate such nested definitions of predicates is given by Avigad [2].
References:
[1] Petr Hájek, Pavel Pudlák: Metamathematics of first-order arithmetic, Springer, 1994, 2nd ed. 1998, 3rd ed. Cambridge Univ. Press 2017.
[2] Jeremy Avigad: Eliminating definitions and Skolem functions in first-order logic, ACM Transactions on Computational Logic 4 (2003), no. 3, pp. 402–415, doi: 10.1145/772062.772068.