# Command lines of verification run A (11 October 2026).
# All programs were run inside this folder with Python 3.13 (lemma4_lp.py needs numpy and scipy; the other programs
# use the standard library only).  The lines below were put together at the writing of the note from the list of
# command lines in the written record of the run and from the arguments that the programs store in their outputs
# (field "args" of the JSON files, first line of the text files); the redirections of the text outputs are those
# of the recorded file names.  The programs with an OUTFILE argument also print one line with the arguments and
# the counts; these lines were collected in out/log_*.txt.  Start and end times of the batches A to G (UTC):
# out/batch*_times.txt; the seconds used by each run are stored in its output.

# single runs
python3 sanity.py > out/sanity.txt
python3 check_example.py > out/check_example.txt
python3 e_vs_f.py > out/e_vs_f.txt

# run_exh.py N K MAXMULT PART NPARTS OUTFILE   (all convex sets, both notions)
python3 run_exh.py 1 1 2 0 1 out/exh_n1_k1_m2.json
python3 run_exh.py 1 2 2 0 1 out/exh_n1_k2_m2.json
python3 run_exh.py 1 3 2 0 1 out/exh_n1_k3_m2.json
python3 run_exh.py 2 1 2 0 1 out/exh_n2_k1_m2.json
python3 run_exh.py 2 2 2 0 1 out/exh_n2_k2_m2.json
python3 run_exh.py 2 3 2 0 1 out/exh_n2_k3_m2.json
python3 run_exh.py 3 1 2 0 1 out/exh_n3_k1_m2.json
python3 run_exh.py 3 2 2 0 1 out/exh_n3_k2_m2.json
python3 run_exh.py 3 3 2 0 1 out/exh_n3_k3_m2.json
python3 run_exh.py 4 1 2 0 1 out/exh_n4_k1_m2.json
python3 run_exh.py 4 2 2 0 1 out/exh_n4_k2_m2.json
python3 run_exh.py 4 3 2 0 4 out/exh_n4_k3_m2_part0.json
python3 run_exh.py 4 3 2 1 4 out/exh_n4_k3_m2_part1.json
python3 run_exh.py 4 3 2 2 4 out/exh_n4_k3_m2_part2.json
python3 run_exh.py 4 3 2 3 4 out/exh_n4_k3_m2_part3.json
python3 run_exh.py 4 4 2 0 3 out/exh_n4_k4_m2_part0.json
python3 run_exh.py 4 4 2 1 3 out/exh_n4_k4_m2_part1.json
python3 run_exh.py 4 4 2 2 3 out/exh_n4_k4_m2_part2.json
python3 run_exh.py 5 3 1 0 3 out/exh_n5_k3_m1_part0.json
python3 run_exh.py 5 3 1 1 3 out/exh_n5_k3_m1_part1.json
python3 run_exh.py 5 3 1 2 3 out/exh_n5_k3_m1_part2.json

# run_exh2.py N K MAXMULT MINSIZE PART NPARTS OUTFILE   (the enumeration convention of original/)
python3 run_exh2.py 3 1 3 1 0 1 out/exh2_n3_k1_m3.json
python3 run_exh2.py 3 2 3 1 0 1 out/exh2_n3_k2_m3.json
python3 run_exh2.py 3 3 3 1 0 1 out/exh2_n3_k3_m3.json
python3 run_exh2.py 3 4 3 1 0 1 out/exh2_n3_k4_m3.json
python3 run_exh2.py 4 1 3 1 0 1 out/exh2_n4_k1_m3.json
python3 run_exh2.py 4 2 3 1 0 1 out/exh2_n4_k2_m3.json
python3 run_exh2.py 4 3 3 1 0 1 out/exh2_n4_k3_m3.json
python3 run_exh2.py 4 4 3 1 0 1 out/exh2_n4_k4_m3.json
python3 run_exh2.py 5 1 1 1 0 1 out/exh2_n5_k1_m1.json
python3 run_exh2.py 5 2 1 1 0 1 out/exh2_n5_k2_m1.json
python3 run_exh2.py 5 3 1 1 0 1 out/exh2_n5_k3_m1.json
python3 run_exh2.py 5 3 2 2 0 2 out/exh2_n5_k3_m2_min2_part0.json
python3 run_exh2.py 5 3 2 2 1 2 out/exh2_n5_k3_m2_min2_part1.json
python3 run_exh2.py 5 4 1 1 0 1 out/exh2_n5_k4_m1.json
python3 run_exh2.py 6 2 1 2 0 1 out/exh2_n6_k2_m1_min2.json
python3 run_exh2.py 6 3 1 2 0 2 out/exh2_n6_k3_m1_min2_part0.json
python3 run_exh2.py 6 3 1 2 1 2 out/exh2_n6_k3_m1_min2_part1.json

# run_rand.py MODE SEED TRIALS OUTFILE [NMIN NMAX]
python3 run_rand.py plain 1 1000000 out/rand_plain_seed1.json
python3 run_rand.py plain 2 1000000 out/rand_plain_seed2.json
python3 run_rand.py minimal 1 300000 out/rand_minimal_seed1.json
python3 run_rand.py minimal 2 300000 out/rand_minimal_seed2.json
python3 run_rand.py minimal 23 8000 out/big_minimal_n10_11_seed23.json 10 11
python3 run_rand.py minimal 24 8000 out/big_minimal_n10_11_seed24.json 10 11
python3 run_rand.py minimal 21 80000 out/big_minimal_n8_9_seed21.json 8 9
python3 run_rand.py minimal 22 80000 out/big_minimal_n8_9_seed22.json 8 9
python3 run_rand.py plain 31 12000 out/big_plain_n8_9_seed31.json 8 9
# (two further runs, "plain" with 8 to 10 vertices, seeds 25 and 26, 100000 trials each, were stopped after
#  20 minutes of CPU time each and left no output: out/batchF_note.txt; the file
#  out/log_big_plain_n8_9_seed32.txt is empty, no result with seed 32 was recorded)

# lemma4_lp.py SEED TRIALS CAP OUTFILE [weak]
python3 lemma4_lp.py 11 20000 400 out/lemma4_strict_seed11.json
python3 lemma4_lp.py 12 20000 400 out/lemma4_weak_seed12.json weak

# nonconvex.py N K MAXMULT;  ffkk_check.py N K MAXMULT
python3 nonconvex.py 3 2 2 > out/nonconvex_n3_k2_m2.txt
python3 nonconvex.py 4 2 2 > out/nonconvex_n4_k2_m2.txt
python3 nonconvex.py 4 3 1 > out/nonconvex_n4_k3_m1.txt
python3 nonconvex.py 5 2 1 > out/nonconvex_n5_k2_m1.txt
python3 ffkk_check.py 3 3 2 > out/ffkk_check_n3_k3_m2.txt
python3 ffkk_check.py 4 2 2 > out/ffkk_check_n4_k2_m2.txt
python3 ffkk_check.py 4 3 2 > out/ffkk_check_n4_k3_m2.txt
python3 ffkk_check.py 5 2 1 > out/ffkk_check_n5_k2_m1.txt

# lemma1_rotation.py M P MAXMULT [PART NPARTS];  lemma1_rotation_rand.py SEED TRIALS MMIN MMAX PMAX
python3 lemma1_rotation.py 2 3 2 > out/lemma1_rotation_m2_p3_x2.txt
python3 lemma1_rotation.py 3 2 2 > out/lemma1_rotation_m3_p2_x2.txt
python3 lemma1_rotation.py 3 3 2 > out/lemma1_rotation_m3_p3_x2.txt
python3 lemma1_rotation.py 3 4 1 > out/lemma1_rotation_m3_p4_x1.txt
python3 lemma1_rotation.py 3 4 2 0 4 > out/lemma1_rotation_m3_p4_x2_part0.txt
python3 lemma1_rotation.py 3 4 2 1 4 > out/lemma1_rotation_m3_p4_x2_part1.txt
python3 lemma1_rotation.py 3 4 2 2 4 > out/lemma1_rotation_m3_p4_x2_part2.txt
python3 lemma1_rotation.py 3 4 2 3 4 > out/lemma1_rotation_m3_p4_x2_part3.txt
python3 lemma1_rotation.py 4 3 1 > out/lemma1_rotation_m4_p3_x1.txt
python3 lemma1_rotation_rand.py 1 60000 4 4 6 > out/lemma1_rotation_rand_m4.txt
python3 lemma1_rotation_rand.py 2 3000 5 5 6 > out/lemma1_rotation_rand_m5.txt

# simple digraphs: run_exh.py with MAXMULT = 1;  simple_rand.py SEED TRIALS NMIN NMAX
python3 run_exh.py 4 3 1 0 1 out/simple_n4_k3.json
python3 run_exh.py 4 4 1 0 1 out/simple_n4_k4.json
python3 run_exh.py 5 2 1 0 1 out/simple_n5_k2.json
python3 simple_rand.py 1 300000 5 7 > out/simple_rand_seed1.txt
python3 simple_rand.py 2 100000 7 8 > out/simple_rand_seed2.txt

# short runs made first, for timing
python3 run_rand.py minimal 0 100 out/test_rand_min.json
python3 run_rand.py plain 0 300 out/test_rand_plain.json
python3 lemma4_lp.py 1 300 400 out/test_lemma4.json

# summary of the JSON outputs (writes out/summary.md)
python3 summarize.py
