# $\overline{SAT} \in NTIME(subexp)$?

Is it possible that $\overline{SAT} \in NTIME(\exp(n^{0.9}))$ ? Are there interesting consequences of such containment? Would it contradict the Exponential Time Hypothesis?

If you use Williams' approach, tightened here, you get a lower bound of $n^{1+\Omega(1)}$ for a function on $n$ bits in the class E$^{NP}$. (For this approach, a fast co-nondeterministic algorithm for satisfibility is sufficient, as you are postulating.) Specifically, the latter paper shows that a lower bound for size $s$ follows from a satisfiability algorithm for circuits of size $O(s)$, which we can translate to a 3SAT instance with $O(s)$ variables by Cook-Levin.
A new preprint by Carmosino et al. introduces the Nondeterministic Strong Exponential Time Hypothesis (NSETH) which makes the conjecture that there are no $\text{NTIME}[2^{(1-\varepsilon) n}]$ algorithms for DNF-TAUT. NSETH is of course an even stronger assumption than "NETH" which you ask about, and still appears to be consistent with everything we know so far. The authors use this conjecture to show that a number of other fine-grained complexity assumptions are unlikely to be reducible to each other.