k=3 n=4: threshold 2; 4 vars, 12 codegree clauses, 1 THC clauses: UNSAT (no counterexample)  [0.0s]
k=3 n=5: threshold 2; 10 vars, 30 codegree clauses, 12 THC clauses: UNSAT (no counterexample)  [0.0s]
k=3 n=6: threshold 3; 20 vars, 90 codegree clauses, 60 THC clauses: UNSAT (no counterexample)  [0.0s]
k=3 n=7: threshold 3; 35 vars, 210 codegree clauses, 360 THC clauses: SAT, counterexample with 23 edges, min codegree 3, THC: False (re-checked by DFS)  [0.0s]
   edges: [[0, 1, 2], [0, 1, 4], [0, 1, 6], [0, 2, 5], [0, 2, 6], [0, 3, 4], [0, 3, 5], [0, 3, 6], [0, 4, 6], [0, 5, 6], [1, 2, 3], [1, 2, 6], [1, 3, 5], [1, 3, 6], [1, 4, 5], [1, 4, 6], [1, 5, 6], [2, 3, 4], [2, 3, 6], [2, 4, 5], [2, 4, 6], [2, 5, 6], [3, 4, 5]]
k=3 n=8: threshold 4; 56 vars, 560 codegree clauses, 2520 THC clauses: UNSAT (no counterexample)  [0.1s]
k=3 n=9: threshold 4; 84 vars, 1260 codegree clauses, 20160 THC clauses: SAT, counterexample with 50 edges, min codegree 4, THC: False (re-checked by DFS)  [0.1s]
   edges: [[0, 1, 2], [0, 1, 3], [0, 1, 7], [0, 1, 8], [0, 2, 4], [0, 2, 5], [0, 2, 6], [0, 3, 5], [0, 3, 6], [0, 3, 8], [0, 4, 5], [0, 4, 6], [0, 4, 8], [0, 5, 7], [0, 6, 7], [0, 7, 8], [1, 2, 3], [1, 2, 7], [1, 2, 8], [1, 3, 7], [1, 3, 8], [1, 4, 5], [1, 4, 6], [1, 4, 7], [1, 4, 8], [1, 5, 6], [1, 5, 7], [1, 5, 8], [1, 6, 7], [1, 6, 8], [2, 3, 5], [2, 3, 6], [2, 3, 7], [2, 4, 5], [2, 4, 6], [2, 4, 7], [2, 5, 8], [2, 6, 8], [2, 7, 8], [3, 4, 5], [3, 4, 6], [3, 4, 7], [3, 4, 8], [3, 5, 6], [3, 7, 8], [4, 7, 8], [5, 6, 7], [5, 6, 8], [5, 7, 8], [6, 7, 8]]
k=4 n=5: threshold 2; 5 vars, 20 codegree clauses, 1 THC clauses: UNSAT (no counterexample)  [0.0s]
k=4 n=6: threshold 2; 15 vars, 60 codegree clauses, 60 THC clauses: UNSAT (no counterexample)  [0.0s]
k=4 n=7: threshold 3; 35 vars, 210 codegree clauses, 360 THC clauses: UNSAT (no counterexample)  [0.0s]
k=4 n=8: threshold 3; 70 vars, 560 codegree clauses, 2520 THC clauses: SAT, counterexample with 49 edges, min codegree 3, THC: False (re-checked by DFS)  [0.0s]
   edges: [[0, 1, 2, 3], [0, 1, 2, 4], [0, 1, 2, 5], [0, 1, 3, 4], [0, 1, 3, 6], [0, 1, 4, 7], [0, 1, 5, 6], [0, 1, 5, 7], [0, 1, 6, 7], [0, 2, 3, 4], [0, 2, 3, 7], [0, 2, 4, 6], [0, 2, 5, 6], [0, 2, 5, 7], [0, 2, 6, 7], [0, 3, 4, 5], [0, 3, 5, 6], [0, 3, 5, 7], [0, 3, 6, 7], [0, 4, 5, 6], [0, 4, 5, 7], [0, 4, 6, 7], [0, 5, 6, 7], [1, 2, 3, 5], [1, 2, 3, 6], [1, 2, 3, 7], [1, 2, 4, 5], [1, 2, 4, 6], [1, 2, 4, 7], [1, 2, 5, 6], [1, 2, 5, 7], [1, 3, 4, 5], [1, 3, 4, 6], [1, 3, 4, 7], [1, 3, 5, 6], [1, 3, 6, 7], [1, 4, 5, 7], [1, 4, 6, 7], [1, 5, 6, 7], [2, 3, 4, 5], [2, 3, 4, 6], [2, 3, 4, 7], [2, 3, 5, 7], [2, 3, 6, 7], [2, 4, 5, 6], [2, 4, 6, 7], [2, 5, 6, 7], [3, 4, 5, 6], [3, 4, 5, 7]]
k=4 n=9: threshold 4; 126 vars, 1680 codegree clauses, 20160 THC clauses: UNSAT (no counterexample)  [14.0s]
k=5 n=6: threshold 2; 6 vars, 30 codegree clauses, 1 THC clauses: UNSAT (no counterexample)  [0.0s]
k=5 n=7: threshold 2; 21 vars, 105 codegree clauses, 360 THC clauses: UNSAT (no counterexample)  [0.0s]
k=5 n=8: threshold 3; 56 vars, 420 codegree clauses, 2520 THC clauses: UNSAT (no counterexample)  [0.0s]
k=5 n=9: threshold 3; 126 vars, 1260 codegree clauses, 20160 THC clauses: SAT, counterexample with 90 edges, min codegree 3, THC: False (re-checked by DFS)  [0.1s]
   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, 4, 5], [0, 1, 2, 4, 6], [0, 1, 2, 4, 7], [0, 1, 2, 4, 8], [0, 1, 2, 5, 6], [0, 1, 2, 5, 7], [0, 1, 2, 5, 8], [0, 1, 2, 6, 7], [0, 1, 2, 6, 8], [0, 1, 2, 7, 8], [0, 1, 3, 4, 5], [0, 1, 3, 4, 6], [0, 1, 3, 5, 8], [0, 1, 3, 6, 7], [0, 1, 3, 7, 8], [0, 1, 4, 5, 7], [0, 1, 4, 6, 8], [0, 1, 4, 7, 8], [0, 1, 5, 6, 7], [0, 1, 5, 6, 8], [0, 2, 3, 4, 5], [0, 2, 3, 4, 6], [0, 2, 3, 5, 8], [0, 2, 3, 6, 7], [0, 2, 3, 7, 8], [0, 2, 4, 5, 7], [0, 2, 4, 6, 8], [0, 2, 4, 7, 8], [0, 2, 5, 6, 7], [0, 2, 5, 6, 8], [0, 3, 4, 5, 6], [0, 3, 4, 5, 7], [0, 3, 4, 5, 8], [0, 3, 4, 6, 7], [0, 3, 4, 6, 8], [0, 3, 4, 7, 8], [0, 3, 5, 6, 7], [0, 3, 5, 6, 8], [0, 3, 5, 7, 8], [0, 3, 6, 7, 8], [0, 4, 5, 6, 7], [0, 4, 5, 6, 8], [0, 4, 5, 7, 8], [0, 4, 6, 7, 8], [0, 5, 6, 7, 8], [1, 2, 3, 4, 5], [1, 2, 3, 4, 6], [1, 2, 3, 5, 8], [1, 2, 3, 6, 7], [1, 2, 3, 7, 8], [1, 2, 4, 5, 7], [1, 2, 4, 6, 8], [1, 2, 4, 7, 8], [1, 2, 5, 6, 7], [1, 2, 5, 6, 8], [1, 3, 4, 5, 6], [1, 3, 4, 5, 7], [1, 3, 4, 5, 8], [1, 3, 4, 6, 7], [1, 3, 4, 6, 8], [1, 3, 4, 7, 8], [1, 3, 5, 6, 7], [1, 3, 5, 6, 8], [1, 3, 5, 7, 8], [1, 3, 6, 7, 8], [1, 4, 5, 6, 7], [1, 4, 5, 6, 8], [1, 4, 5, 7, 8], [1, 4, 6, 7, 8], [1, 5, 6, 7, 8], [2, 3, 4, 5, 6], [2, 3, 4, 5, 7], [2, 3, 4, 5, 8], [2, 3, 4, 6, 7], [2, 3, 4, 6, 8], [2, 3, 4, 7, 8], [2, 3, 5, 6, 7], [2, 3, 5, 6, 8], [2, 3, 5, 7, 8], [2, 3, 6, 7, 8], [2, 4, 5, 6, 7], [2, 4, 5, 6, 8], [2, 4, 5, 7, 8], [2, 4, 6, 7, 8], [2, 5, 6, 7, 8]]
k=6 n=7: threshold 2; 7 vars, 42 codegree clauses, 1 THC clauses: UNSAT (no counterexample)  [0.0s]
k=6 n=8: threshold 2; 28 vars, 168 codegree clauses, 2520 THC clauses: UNSAT (no counterexample)  [0.0s]
k=6 n=9: threshold 3; 84 vars, 756 codegree clauses, 20160 THC clauses: UNSAT (no counterexample)  [0.1s]
k=7 n=8: threshold 2; 8 vars, 56 codegree clauses, 1 THC clauses: UNSAT (no counterexample)  [0.0s]
k=7 n=9: threshold 2; 36 vars, 252 codegree clauses, 20160 THC clauses: UNSAT (no counterexample)  [0.1s]
