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

v1.1.0 (15 Aug 2026): Z15 resolved. This version adds the LRAT certificate that closes the 15-point case; the description below covers the complete dataset. 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, 14 or 15 points violates the conjecture. Each case is decided by two independent exact methods (OR-Tools CP-SAT with a native integer margin constraint, and CaDiCaL on an independently written CNF encoding) and carries a machine-verified proof certificate: DRAT verified by drat-trim for Z14 (s VERIFIED; 3,411,578 core lemmas, 315,224,851 resolution steps), and streaming-verifiable LRAT verified by lrat-check for Z15 (c VERIFIED in 22.6 minutes on a 16 GB machine — the format switch that dissolved v1.0.0's verifier memory wall). Together with the sequel repository frankl-transitive-sat (datasets: doi:10.5281/zenodo.21920979), the transitive case of the conjecture is closed up to 15 points. Files (xz-compressed; integrity anchors in SHA256SUMS.txt and z15.lrat.sha256): 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 Z14 (2.24 GB decompressed); z15min3.cnf.xz — the Z15 instance (p cnf 16856 28850111), deterministic output of dump_dimacs.py 15 z15min3.cnf 3, sha256 of the decompressed file e6c732cf30bc619dd4c2706734bdcc2ed99255a422c52c4a8525563785115120 — the exact input of the certified refutation below; z15.lrat.xz — the verified LRAT unsatisfiability certificate for Z15 (147 GB decompressed, 158,233,546,333 bytes; sha256 of the decompressed proof 9d8b6b722236cd45da5a604494d0f12072e30a163268aab58ee14d6e83ec0dd3, recorded in z15.lrat.sha256). Produced by CaDiCaL 3.0.1 (--lrat --no-binary) in a single unbounded 20 h 26 m run; Z15-RESOLVED.md — the full evidence chain and re-verification commands; SHA256SUMS.txt, z15.lrat.sha256 — integrity anchors. Verification recipes. Z14: unxz both z14 files, check hashes, run drat-trim z14min3.cnf z14min3.drat (~30 minutes, <2 GB RAM); expect s VERIFIED. Z15: unxz both z15 files, check hashes, run lrat-check z15min3.cnf z15.lrat (~23 minutes; forward streaming, RAM tracks the formula, not the 147 GB proof); expect the line c VERIFIED — never trust exit codes alone. The partial DRAT trace of v1.0.0's interrupted Z15 run remains deliberately not archived: a truncated trace certifies nothing. Full mathematical statements, measured resource data, reproduction instructions and the remaining open problems: see the repository's README.md and docs/. The computations were carried out with Anthropic's Claude Code (model claude-fable-5, no fallback) — the v1.0.0 campaign by an autonomous agent loop, the v1.1.0 resolution in interactive sessions — under human supervision, on one 16 GB laptop and a consumer Claude subscription (Max 20×).