Are there any statements $\phi$ where "$\vdash \phi$ or $\vdash \neg \phi$" was shown nonconstructively?

Question

I am wondering if there is an example of a statement $\phi$ in the language of some formal system $T$ satisfying (1-4):

1. $\phi$ was shown to not be independent of $T$ (i.e. it was proved that $T \vdash \phi$ or $T \vdash \neg \phi$)
2. The proof in (1) was nonconstructive: it was initially (or still) unknown which of {$\phi, \neg \phi$} was a theorem of $T$.
3. $\phi$ was not clearly $\Delta_0$ (any bounded statement like "there is no odd perfect number less than 10↑↑↑10" has a (possibly long) proof/disproof).
4. $\phi$ was not part of some class of statements $C$ that were shown by some algorithm to be decidable. (For instance, any statement in Presburger arithmetic or ACF/RCF which we know to be decidable by a quantifier elimination algorithm).
5. $T$ is r.e.