Near-threshold exponential resolution lower-bound conjecture for Term Coding

Let $\Gamma\cup L$ be a single-sorted Term Coding problem, where $\Gamma$ is a set of term equations and $L$ is a set of non-equality constraints, over an $n$-element alphabet. Define the set of solvable domain sizes

$$S=\{m\in\mathbb{N}:\Gamma\cup L\text{ has a solution for domain size }m\}.$$

Near-threshold resolution lower-bound conjecture. For an instance size $n$ with no solution, $n\notin S$, if

$$\operatorname{dist}(n,S)=\min_{m\in S}|n-m|\leq\log^{O(1)}(n),$$

then any resolution-based proof certifying non-existence of a solution for size $n$ via the corresponding SAT instance $\{\mathrm{SAT}\}_{\Gamma,L}$ must have exponential size.

This conjecture concerns proof-complexity barriers near a solvability threshold. It is motivated by the stated dichotomy between polynomial-size proofs and failure in every infinite model, together with classical exponential resolution lower bounds; the source supplies no resolution of the conjecture.