Polynomial-time computation of autarkies beyond the lean minimum-degree bound

Let $F$ be a clause-set with deficiency surplus $\operatorname{\sigma}(F) \ge 1$. Write $\mu\\!\operatorname{vd}(F)$ for its minimum variable-degree and $\operatorname{nM}(k)$ for the non-Mersenne bound. Autarky-computation conjecture. If $\mu\\!\operatorname{vd}(F) > \operatorname{nM}(\operatorname{\sigma}(F))$, then a non-trivial autarky for $F$ can be computed by a polynomial-time algorithm. The preceding theorem guarantees the existence of such an autarky, but the efficient computation of the autarky itself remains open.