Clean rerun of the search code (2026-10-01; Python 3.13.5, python-sat 1.9.dev15, Apple clang 21, macOS arm64)

All scripts of search/ were copied to an empty directory (without results/ and certs/), the checkers
tools/drat_check.c and tools/drat_check2.c were recompiled, and everything was run again.  The same was then
repeated from a fresh copy of this package (paths as in the package).

Explicit constructions (output compared byte for byte with the recorded output: identical)
  verify_example7.py        -> verify_example7.out
  verify_orientable10.py    -> verify_orientable10.out
  glue.py                   -> results/glue_chain7.out, results/chain7.json
  example12.py              -> results/example12.out
  holmes_check.py           -> results/holmes_check.out

Certificates (certify.py; the formula and the DRAT proof compared by sha256 with the recorded ones: identical)
  n4_D2 n5_D3 n6_D4 n7_D6 n8_D7 n9_D8 n5_D3_orientable n6_D4_orientable n7_D5_orientable
  n8_D6_orientable n9_D7_orientable                      -> identical to certificates/*.gz
  n10_D9, n10_D9_orientable                              -> identical to the sha256 recorded at the first run
                                                            (certificates/n10_certificates.txt)
  certify_unique7.py -> results/certify_unique7.out identical; unique_n7_D5.cnf/.drat identical
  audit/certify_enum.py ../search 8 6 -> enum_n8_D6.cnf/.drat identical to certificates/enum_n8_D6.*

Enumerations and cross-checks (outputs identical)
  enumerate7.py 7 5         -> results/enumerate_n7_D5.out   (4 labelled complexes, 1 class)
  enumerate7.py 8 6         -> results/enumerate_n8_D6.out   (16 labelled complexes, 2 classes)
  enumerate7_triage_encoding.py -> results/enumerate_n7_D5_triage_encoding.out (72 labelled, 1 class)
  checker_selftest.py       -> results/checker_selftest.out
  recheck_certs.sh          -> results/recheck_certs.out (all VERIFIED by drat_check and drat_check2)

Closed surfaces (satsearch.py n n-2 --closed), rerun for n = 4..9: UNSAT for every n, as recorded in
results/closed_check.out (n = 10 not rerun).  Sanity check: satsearch.py 6 3 --closed is SAT (a 6-vertex
2-sphere with dual diameter 3).

Uncertified n = 11 runs (CaDiCaL 1.9.5, satsearch.py; recorded run / rerun):
  satsearch.py 11 10               UNSAT, 546 lazy iterations; 1582.3 s / 1601.0 s
  satsearch.py 11 10 --orientable  UNSAT, 423 lazy iterations; 2643.3 s / 2469.5 s
  satsearch.py 11 9                SAT (dual diameter 9, chi = -10, non-orientable), 0.2 s
  satsearch.py 11 9 --orientable   SAT (dual diameter 9, chi = -4, orientable), 110.8 s
These UNSAT answers carry no certificate.
