If the ordering over undecidable theories by their efficiency at proving tautologies exactly coincides with some familiar logical strength measure, our deep understanding of when one theory cannot prove the consistency of or interpret another would, we show, fully characterize theories’ hard-to-prove tautology families. It has been ruled out that “theory S is less efficient at proving tautologies than any theory S+$\phi$ proving strictly more sentences”; a counterexample is any $\phi$ such that S efficiently interprets S+$\phi$, where $\phi$ might be a certain Rosser sentence. The literature has not considered fallback conjectures, such as “theory S is less efficient at proving tautologies than S+$\phi$ if and only if S does not efficiently interpret S+$\phi$”. Such conjectures assert an alignment between complexity theory and logic that translates textbook impossibility results (“S does not efficiently interpret S+$\phi$”) into hard tautologies (tautologies encoding “S+$\phi$ lacks a length $n$ proof of $0 =1$” are hard to prove in S). We discuss which familiar orders over theories seem likely and which can be ruled out.