I was able to [reproduce Mathias's results with some Haskell code](https://gist.github.com/pqnelson/184a13964b5560eac73d821309c5c081) with some specific details about how many symbols are needed in each term. (As a sanity check, I verified I recovered the same results term-by-term when the ordered product was primitive.)

 - Size of 1 = 2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897
 - Size of term A = 15,756,227
 - Size of term B = 10,006,221,599,868,316,846
 - Size of term C = 59,308,566,315
 - Size of term D = 364,936,653,508,895,574,881
 - Size of term E = 101,217,516,631

One thing worth noting is that, well, this seems dishonest. I mean, there are a lot of double negations which are not simplified, which bloats the size quite a bit (an additional $1.863\times 10^{53}$ symbols or so). I wouldn't be surprised if there were other simplifications which would cut down the bloat further...not that we'd get anything less than $10^{50}$ or so.

If you'd like to check the number of links, I can do that too.