I was able to reproduce Mathias's results with some Haskell code with some specific details about how many symbols are needed in each term. (As a sanity check, I verified I recovered the same results reported by Mathias term-by-term when the ordered product was primitive.)
When the ordered pair is not primitive, the sizes of the various terms are:
- 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.
Addendum. The relation "1+1=2" can be computed, and found to have a length of 22,411,322,875,029,037,193,545,441,224,646,148,573,589,725,893,763,139,344,694,162,029,240,084,343,041 (or approximately $2.24113228750290371 \times 10^{76}$). This is using the definitions in Bourbaki of cardinal addition $\mathfrak{a}+\mathfrak{b}$ using the disjoint sum of the indexed family $f\colon\mathrm{Card}(2)\to\{\mathfrak{a},\mathfrak{b}\}$ considered as a graph. It's really convoluted, but the details can be found in Bourbaki's Theory of Sets Chapter II sections 3.4, 4.1, and 4.8 as well as Proposition 5 (in chapter III, section 3.3); this all works with the Kuratowski ordered pair, not a primitive $\bullet A B$ ordered pair.
For what it's worth, computing the size of 1 was nearly instantaneous, whereas computing the size of "1+1=2" took about 7 minutes and 30 seconds.