Actually, I would be more interested in the size of checking core of Qea. Quickly inspecting 23 megabytes of proofs sounds like a bad idea. A converter to TSTP first-order proof format (for example) would allow me to use a few different bug-for-bug-independent well-tested checkers for this format that are already out there; that I would trust more than both human inspection and any single-implementation prover.