Checks of the two n = 10 certificates (regenerated from a clean copy of the search code;
sha256 as in ../../certificates/n10_certificates.txt).

== n10_D9 ==
search/certify.py: result UNSAT, 204 lazy iterations, 97524 clauses, 2545 variables, solve time 71.1 s, proof lines 3125658
sha256 cnf  eb31f84fda4abbc907a672d74e97cdc815c8d1efdbbd9f05bb35ea5ac70a46f9
sha256 drat 981f0ccea17976710a4f242624938dcd393b57e8cd0854d7fbf3bfce90a2daa6
-- search/tools/drat_check2 (forward DRAT, deletions applied), 114.8 s:
   c formula: 2545 vars, 97524 clauses read (header 97524)
   c lemmas checked: 1609977 (RAT: 0), deletions: 1515354 (not found: 326)
   s VERIFIED
-- audit/rupcheck -d (deletions applied):
   c formula: 97524 clauses read (header: 2545 vars, 97524 clauses)
   c lemmas checked: 1609977; deletions applied: 1515354, ignored: 0, not found: 326; mode: deletions applied (non-unit)
   s VERIFIED
   wall time 126.76 s
-- audit/rupcheck (deletions ignored):
   c formula: 97524 clauses read (header: 2545 vars, 97524 clauses)
   c lemmas checked: 1609977; deletions applied: 0, ignored: 1515680, not found: 0; mode: deletions ignored
   s VERIFIED
   wall time 1156.12 s
-- audit/cnf_audit.py:
   file n10_D9.cnf: n=10 D=9 orientable=False | vars 2545 | clauses 97524 = base 95426 + link cuts 2098 + blocking 0
   AUDIT PASS

== n10_D9_orientable ==
search/certify.py: result UNSAT, 176 lazy iterations, 99960 clauses, 2665 variables, solve time 63.9 s, proof lines 2863487
sha256 cnf  a9c517ef3717ab275e2862fd9c5e9f68cd0dc953136f06c0c7337f108dc56646
sha256 drat bfb60eca8e1a40ee109ad694d3a048d607c651c612be72447173422c1ce879be
-- search/tools/drat_check2 (forward DRAT, deletions applied), 102.2 s:
   c formula: 2665 vars, 99960 clauses read (header 99960)
   c lemmas checked: 1448064 (RAT: 0), deletions: 1415097 (not found: 325)
   s VERIFIED
-- audit/rupcheck -d (deletions applied):
   c formula: 99960 clauses read (header: 2665 vars, 99960 clauses)
   c lemmas checked: 1448064; deletions applied: 1415097, ignored: 0, not found: 325; mode: deletions applied (non-unit)
   s VERIFIED
   wall time 111.77 s
-- audit/rupcheck (deletions ignored):
   c formula: 99960 clauses read (header: 2665 vars, 99960 clauses)
   c lemmas checked: 1448064; deletions applied: 0, ignored: 1415422, not found: 0; mode: deletions ignored
   s VERIFIED
   wall time 979.71 s
-- audit/cnf_audit.py:
   file n10_D9_orientable.cnf: n=10 D=9 orientable=True | vars 2665 | clauses 99960 = base 97946 + link cuts 2014 + blocking 0
   AUDIT PASS
