Are there strongly normalizing lambda terms that cannot be given a System F type?
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).