Does every NO instance of this promise problem have a local refutation?

Question

For the following equivalent questions, you choose
whether-or-not the 3 variables in a clause must be distinct.

Is there an integer $k$ such that for all 3-SAT formulas $\mathcal{F}$ without negations,
if every ​ $(\leq k)$-clause sub-formula of $\mathcal{F}$ is 1-in-3 satisfiable then $\mathcal{F}$ is NAE-satisfiable?

Equivalently, is there an integer $k$ such that for all
3-SAT formulas $\mathcal{F}$ without negations, if $\mathcal{F}$ is not NAE-satisfiable then
$\mathcal{F}$ has a ​ $(\leq k)$-clause sub-formula which is not 1-in-3 satisfiable?

(The Fano plane shows that $k$ can't be less than $7$.)

Motivation: ​ ​ ​ That is the "low end" of my question
on cs.stackexchange which was inspired by the
possibility of generalizing Schaefer's dichotomy theorem
to constraint satisfaction promise problems.
Specifically, for the simplest non-trivial promise-constraint,
with m being the size of the input set, I have neither managed to
find evidence for it being in ​ promisecoQIP[2]TIME$\hspace{-0.02 in}\big(\hspace{-0.04 in}$2^o(m)$\hspace{-0.03 in}\big)\hspace{-0.04 in}\big/\hspace{-0.04 in}$q2^o(m)
for infinitely many m, nor find evidence that it's not solvable
in coNTIME(O(1)) on essentially the most basic word RAM.
The former applies even when each variable occurs exactly twice
and "many m" gets replaced with "many even m" (since 3 is odd),
and the latter applies even when negative literals are allowed.

Answer 1

So if I understood well, your problem in the language of graph theory would be as follows:

Is there a $k$ such that if for a $3$-uniform hypergraph for any $k$ of its edges we can select a $1$-shallow hitting set (a set of vertices that meets each of the $k$ edges in exactly one vertex), then the hypergraph is $2$-colorable?

The answer to this question is no because for any $g$ and $r$ there are $r$-uniform hypergraphs of girth $g$ with arbitrarily high chromatic number [Kostochka-Nesetril]. The girth $g$ of an $r$-uniform hypergraph is the smallest $g$ for which there are $g-1$ edges whose union has size at most $g(k-1)$. Thus, if a hypergraph has girth $g$, then any $g-1$ edges have a $1$-shallow hitting set by induction because their union looks like a tree. This means that locally it satisfies your 1-in-3 satisfiability condition, but it is not $2$-colorable, so there is no NAE-satisfying assignment for the whole hypergraph.