| PNs | term | wc | gzip | ||
| ZFC | 32 | 1570 | 2232 | 774 | |
| new foundations | 37 | 972 | 1800 | 640 | |
| Isabelle/Pure | 23 | 1200 | 1632 | 532 | |
| HOL Light logic | 24 | 2793 | 3251 | 903 | |
| calculus of constructions | 30 | 784 | 1409 | 515 | |
| ECC | 46 | 1636 | 2399 | 696 | |
| extensional MLW | 77 | 3808 | 5219 | 1171 | |
| category theory | 45 | 2601 | 4076 | 1153 | |
| categorical set theory | 38 | 3794 | 4944 | 1518 |