It may be the case in first-order logic that to decide whether \(E\vdash ^{\texttt {t}} A\) and \(E\not \vdash ^{\texttt {t}} \lnot B,\) there are infinitely many stages s such that \(E\vdash ^{\texttt {t}}_s A\) and \(E\not \vdash ^{\texttt {t}}_s \lnot B,\) and infinitely many stages s such that either \(E\not \vdash ^{\texttt {t}}_s A\) or \(E\vdash ^{\texttt {t}}_s \lnot B.\) This will restrain formulas enumerated into or extracted from E,  which results in too many formulas from E or into E.