 Let \(F\) be the propositional formula  \[  ( ( \neg \neg D \rightarrow D) \rightarrow ( \neg \neg D \vee \neg D ) ) \rightarrow ( \neg \neg D \vee \neg D)  \]  where \(D\) is \((\neg P \vee \neg Q)\) and \(P,\) \(Q\) are prime. Every arithmetical substitution instance of \(F\) is realizable (using classical logic), but \(F\) is not provable in \(\mathbf{IPC}.\)