> The particular problem in HOL is the main function, which has > 161,783 blocks and 257,519 variables -- the product of those two > numbers being about 860 million. Correction: the product of those two numbers is about 41 billion. Now, we're not likely going to need that much space since we use a sparse representation. But even 1/100th would really hurt. And of course this rules out bit vectors.