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

>Is there an integer $k$ such that for all [3-SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability) formulas $\mathcal{F}$ without negations,
<br>
if every ​ $(\leq k)$-clause sub-formula of $\mathcal{F}$ is [1-in-3](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Exactly-1_3-satisfiability) satisfiable then $\mathcal{F}$ is [NAE](http://blog.geomblog.org/2008/03/joys-of-nae-sat.html)-satisfiable?
<br><br>
Equivalently, is there an integer $k$ such that for all
<br>
[3-SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability) formulas $\mathcal{F}$ without negations, if $\mathcal{F}$ is not [NAE](http://blog.geomblog.org/2008/03/joys-of-nae-sat.html)-satisfiable then
<br>
$\mathcal{F}$ has a ​ $(\leq k)$-clause sub-formula which is not [1-in-3](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Exactly-1_3-satisfiability) satisfiable?

(The [Fano plane](https://en.wikipedia.org/wiki/Fano_plane) shows that $k$ can't be less than $7$.)

<br>
**Motivation:** ​ ​ ​ That is the "low end" of my question
<br>
[on cs.stackexchange](http://cs.stackexchange.com/q/51828/12859) which was inspired by the
<br>
possibility of generalizing [Schaefer's dichotomy theorem](https://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem)
<br>
to constraint satisfaction [promise](https://en.wikipedia.org/wiki/Promise_problem) problems.
<br>
Specifically, for _the simplest_ non-trivial promise-constraint,
<br>
with m being the size of the input set, I have neither managed to
<br>
find evidence for it being in ​ [promise](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:P#promisebqp)co[QIP\[2\]](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:Q#qip2)T[IME](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:N#ntime)$\hspace{-0.02 in}\big(\hspace{-0.04 in}$2<sup>[o](https://en.wikipedia.org/wiki/Big_O_notation#Little-o_notation)(m)</sup>$\hspace{-0.03 in}\big)\hspace{-0.04 in}\big/\hspace{-0.04 in}$[q](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:Q#qmaqpoly)2<sup>[o](https://en.wikipedia.org/wiki/Big_O_notation#Little-o_notation)(m)</sup>
<br>
for infinitely many m, nor find evidence that it's not solvable
<br>
in [co](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:C#conp)N[TIME](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:N#ntime)(O(1)) on essentially the most basic [word RAM](https://duckduckgo.com/?q=%22word+RAM%22+complexity).
<br>
The former applies even when each variable occurs exactly twice
<br>
and "many m" gets replaced with "many _even_ m" (since 3 is odd),
<br>
and the latter applies even when [negative literals](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Basic_definitions_and_terminology) are allowed.<br><br>