I have a couple of experiences of doing similar big projects where we counted the number of some objects (I haven't checked how big they are.. I have run SAT solvers for a couple of weeks, I didn't try to record some "proof size", I imagine it would be as big if not bigger than 200 terabytes).

Once I could tell a mathematician the count, in both cases someone they proved the result in an alternative way fairly soon afterwards :)