Certificate ledgers

The machine-checked evidence for the certified claims. Each line of a ledger records one SAT query: the statement and cell it encodes, the SHA-256 of the CNF formula, the solver's verdict, and, where a proof was produced, the size and SHA-256 of the DRAT proof and the verdict of the independent checker drat-trim. A query with verdict UNSAT and a DRAT proof verified by drat-trim is a machine-checked proof that no state of the kind encoded exists on that cell. Queries without a proof (for instance pre-flight runs) are solver verdicts only. The formulas and proofs themselves (hundreds of megabytes to gigabytes) are not published; they are regenerated by the scripts named on the claim pages and checked against the hashes in the *_sha256_*.txt files. The statement letters and tags are those of the ledgers; the claim pages and the campaign reports explain them.

Counts below are computed from the ledgers when the site is built.