# referee_census_sat.py census <k> 10 3000, run by the referee; assembled by the lead auditor on 2026-09-28 from
# the referee's per-k output files after the runs ended. The k=4 run ended without printing a result after
# about 62 minutes (no answer): (4,10) is undecided.
k=3 n=10: threshold 5; 120 vars, 3150 codegree clauses, 181440 THC clauses: UNDECIDED (timeout 3000.0s)
k=4 n=10: threshold 3; no output (run stopped without an answer)
k=5 n=10: threshold 4; 252 vars, 4200 codegree clauses, 181440 THC clauses: SAT, counterexample with 186 edges, min codegree 4, THC: False (re-checked by DFS)  [1.3s]
   edges: [[0, 1, 2, 3, 4], [0, 1, 2, 3, 5], [0, 1, 2, 3, 6], [0, 1, 2, 3, 7], [0, 1, 2, 3, 8], [0, 1, 2, 3, 9], [0, 1, 2, 4, 5], [0, 1, 2, 4, 6], [0, 1, 2, 4, 7], [0, 1, 2, 4, 8], [0, 1, 2, 4, 9], [0, 1, 2, 5, 6], [0, 1, 2, 5, 7], [0, 1, 2, 5, 8], [0, 1, 2, 5, 9], [0, 1, 2, 6, 7], [0, 1, 2, 6, 8], [0, 1, 2, 6, 9], [0, 1, 2, 7, 8], [0, 1, 2, 7, 9], [0, 1, 2, 8, 9], [0, 1, 3, 4, 5], [0, 1, 3, 4, 6], [0, 1, 3, 4, 7], [0, 1, 3, 4, 8], [0, 1, 3, 4, 9], [0, 1, 3, 5, 6], [0, 1, 3, 5, 7], [0, 1, 3, 5, 8], [0, 1, 3, 5, 9], [0, 1, 3, 6, 7], [0, 1, 3, 6, 8], [0, 1, 3, 6, 9], [0, 1, 3, 7, 8], [0, 1, 3, 7, 9], [0, 1, 3, 8, 9], [0, 1, 4, 5, 6], [0, 1, 4, 5, 7], [0, 1, 4, 6, 9], [0, 1, 4, 7, 8], [0, 1, 4, 8, 9], [0, 1, 5, 6, 8], [0, 1, 5, 7, 9], [0, 1, 5, 8, 9], [0, 1, 6, 7, 8], [0, 1, 6, 7, 9], [0, 2, 3, 4, 5], [0, 2, 3, 4, 6], [0, 2, 3, 4, 7], [0, 2, 3, 4, 8], [0, 2, 3, 4, 9], [0, 2, 3, 5, 6], [0, 2, 3, 5, 7], [0, 2, 3, 5, 8], [0, 2, 3, 5, 9], [0, 2, 3, 6, 7], [0, 2, 3, 6, 8], [0, 2, 3, 6, 9], [0, 2, 3, 7, 8], [0, 2, 3, 7, 9], [0, 2, 3, 8, 9], [0, 2, 4, 5, 8], [0, 2, 4, 5, 9], [0, 2, 4, 6, 7], [0, 2, 4, 6, 8], [0, 2, 4, 7, 9], [0, 2, 5, 6, 7], [0, 2, 5, 6, 9], [0, 2, 5, 7, 8], [0, 2, 6, 8, 9], [0, 2, 7, 8, 9], [0, 3, 4, 5, 6], [0, 3, 4, 5, 9], [0, 3, 4, 6, 8], [0, 3, 4, 7, 8], [0, 3, 4, 7, 9], [0, 3, 5, 6, 7], [0, 3, 5, 7, 8], [0, 3, 5, 8, 9], [0, 3, 6, 7, 9], [0, 3, 6, 8, 9], [0, 4, 5, 6, 7], [0, 4, 5, 6, 8], [0, 4, 5, 6, 9], [0, 4, 5, 7, 8], [0, 4, 5, 7, 9], [0, 4, 5, 8, 9], [0, 4, 6, 7, 8], [0, 4, 6, 7, 9], [0, 4, 6, 8, 9], [0, 4, 7, 8, 9], [0, 5, 6, 7, 8], [0, 5, 6, 7, 9], [0, 5, 6, 8, 9], [0, 5, 7, 8, 9], [0, 6, 7, 8, 9], [1, 2, 3, 4, 5], [1, 2, 3, 4, 6], [1, 2, 3, 4, 7], [1, 2, 3, 4, 8], [1, 2, 3, 4, 9], [1, 2, 3, 5, 6], [1, 2, 3, 5, 7], [1, 2, 3, 5, 8], [1, 2, 3, 5, 9], [1, 2, 3, 6, 7], [1, 2, 3, 6, 8], [1, 2, 3, 6, 9], [1, 2, 3, 7, 8], [1, 2, 3, 7, 9], [1, 2, 3, 8, 9], [1, 2, 4, 5, 6], [1, 2, 4, 5, 9], [1, 2, 4, 6, 8], [1, 2, 4, 7, 8], [1, 2, 4, 7, 9], [1, 2, 5, 6, 7], [1, 2, 5, 7, 8], [1, 2, 5, 8, 9], [1, 2, 6, 7, 9], [1, 2, 6, 8, 9], [1, 3, 4, 5, 8], [1, 3, 4, 5, 9], [1, 3, 4, 6, 7], [1, 3, 4, 6, 8], [1, 3, 4, 7, 9], [1, 3, 5, 6, 7], [1, 3, 5, 6, 9], [1, 3, 5, 7, 8], [1, 3, 6, 8, 9], [1, 3, 7, 8, 9], [1, 4, 5, 6, 7], [1, 4, 5, 6, 8], [1, 4, 5, 6, 9], [1, 4, 5, 7, 8], [1, 4, 5, 7, 9], [1, 4, 5, 8, 9], [1, 4, 6, 7, 8], [1, 4, 6, 7, 9], [1, 4, 6, 8, 9], [1, 4, 7, 8, 9], [1, 5, 6, 7, 8], [1, 5, 6, 7, 9], [1, 5, 6, 8, 9], [1, 5, 7, 8, 9], [1, 6, 7, 8, 9], [2, 3, 4, 5, 6], [2, 3, 4, 5, 7], [2, 3, 4, 6, 9], [2, 3, 4, 7, 8], [2, 3, 4, 8, 9], [2, 3, 5, 6, 8], [2, 3, 5, 7, 9], [2, 3, 5, 8, 9], [2, 3, 6, 7, 8], [2, 3, 6, 7, 9], [2, 4, 5, 6, 7], [2, 4, 5, 6, 8], [2, 4, 5, 6, 9], [2, 4, 5, 7, 8], [2, 4, 5, 7, 9], [2, 4, 5, 8, 9], [2, 4, 6, 7, 8], [2, 4, 6, 7, 9], [2, 4, 6, 8, 9], [2, 4, 7, 8, 9], [2, 5, 6, 7, 8], [2, 5, 6, 7, 9], [2, 5, 6, 8, 9], [2, 5, 7, 8, 9], [2, 6, 7, 8, 9], [3, 4, 5, 6, 7], [3, 4, 5, 6, 8], [3, 4, 5, 6, 9], [3, 4, 5, 7, 8], [3, 4, 5, 7, 9], [3, 4, 5, 8, 9], [3, 4, 6, 7, 8], [3, 4, 6, 7, 9], [3, 4, 6, 8, 9], [3, 4, 7, 8, 9], [3, 5, 6, 7, 8], [3, 5, 6, 7, 9], [3, 5, 6, 8, 9], [3, 5, 7, 8, 9], [3, 6, 7, 8, 9]]
k=6 n=10: threshold 3; 210 vars, 2520 codegree clauses, 181440 THC clauses: UNDECIDED (timeout 3000.0s)
k=7 n=10: threshold 3; 120 vars, 1260 codegree clauses, 181440 THC clauses: UNSAT (no counterexample)  [1.3s]
