Certified SAT artifacts for Frankl's union-closed sets conjecture under cyclic symmetry (Z14 DRAT certificate; Z14/Z15 CNF instances)

Heavy computational artifacts supporting the repository frankl-cyclic-sat: a computer-assisted decision of the rotation-invariant case of Frankl's union-closed sets conjecture. No rotation-invariant union-closed family on 13 or 14 points violates the conjecture; both cases are decided by two independent exact methods (OR-Tools CP-SAT and CaDiCaL on independent encodings) and the 14-point refutation carries the DRAT certificate archived here, verified with drat-trim (s VERIFIED; 3,411,578 core lemmas, 315,224,851 resolution steps). Files (xz-compressed; SHA-256 of both compressed and original bytes in SHA256SUMS.txt): z14min3.cnf.xz — the Z14 instance (p cnf 5184 7342059), deterministic output of the repository's dump_dimacs.py 14 z14min3.cnf 3; z14min3.drat.xz — the verified DRAT unsatisfiability certificate for the Z14 instance (2.24 GB decompressed); z15min3.cnf.xz — the Z15 instance (p cnf 16856 28850111). CP-SAT reports it infeasible (no rotation-invariant counterexample on 15 points), but independent SAT confirmation is still open: this file is the exact input for anyone who wants to complete that validation; SHA256SUMS.txt — integrity anchors. Verification recipe (Z14): unxz both z14 files, check hashes against SHA256SUMS.txt, then run drat-trim z14min3.cnf z14min3.drat (~30 minutes, <2 GB RAM); expected output s VERIFIED. The partial DRAT trace of the interrupted Z15 run is deliberately not archived: a truncated trace certifies nothing. Full mathematical statements, measured resource data, reproduction instructions and open problems: see the repository's README.md and docs/. The computations were executed autonomously by an AI agent loop built on Anthropic's Claude Code under human supervision.