An improved time‐space lower bound for tautologies

We show that for all reals c and d such that c ² d <4 there exists a positive real e such that tautologies of length n cannot be decided by both a nondeterministic algorithm that runs in time n ^c , and a nondeterministic algorithm that runs in time n ^d and space n ^e . In particular, for every $d\text{Unknown character}\sqrt{[}3]4$ there exists a positive e such that tautologies cannot be decided by a nondeterministic algorithm that runs in time n ^d and space n ^e .