Are there strongly normalizing lambda terms that cannot be given a System F type? I know that all well-typed System F terms are strongly normalizing, but is the converse true as well? In other words, does System F typeability precisely characterize program termination? (And if so, how to prove it?) Or are there lambda terms that are strongly normalizing but cannot be given a System F type?
A System F interpreter cannot be implemented in System F. On the other hand, a System F interpreter can be implemented in untyped lambda calculus, but that's not enough. Can a strongly normalizing System F interpreter be implemented in untyped lambda calculus? If yes, this answers our question positively, but I am not sure about it.
As you found out yourself, the answer to your question is yes.  You found a rather convoluted example, a much simpler example is the following:
$$(\lambda zy.y(zI)(zK))(\lambda x.xx)$$
where $I$ and $K$ are the identity and first-projection combinators.  This may be found at p. 204 of Sørensen and Urzyczyn's Lectures on the Curry-Howard Isomoprphism.  They attribute it to Ronchi Della Rocca and Giannini, and also give a seemingly even simpler example, which is $c_2c_2K$, where $c_2$ is, I believe, the Church integer 2 (I'm not sure about their notation so I may be wrong).