For such standard definitions it will also be the case that for each \(n\), there will be of order \(O(2^n)\) \(\mathsf{T}\)-derivations of length \(n = \lvert \mathcal{D}\rvert\) (say measured in the number of symbols in \(\mathcal{D}\)). We can thus non-deterministically check if \(\phi\) is derivable by a proof of size \(\leq n\) by guessing a sequence of symbols length \(n\) and then checking (in polynomial time) whether it is a well-formed proof of \(\phi\). It thus follows that the following problem is in \(\textbf{NP}\):