#!/bin/sh
# Runs drat-trim (via check_fortcover_proof.py, with execution logging) on the stored
# fort-cover proofs for n = 23 and n = 25 in parallel. Called by reproduce.sh (FULL=1) and
# used in the Stage 8 revision; see review/revisions.md (F1).
cd "$(dirname "$0")/../.."
export PYTHONPATH=.pydeps:code
mkdir -p results/revision
python3 code/tools/logrun.py check_fortcover_proof_n23 --log results/revision/check_fortcover_n23.log -- python3 code/check_fortcover_proof.py 23 11 14400 &
P1=$!
python3 code/tools/logrun.py check_fortcover_proof_n25 --log results/revision/check_fortcover_n25.log -- python3 code/check_fortcover_proof.py 25 11 18000 &
P2=$!
wait $P1; E1=$?
wait $P2; E2=$?
echo "n23 exit=$E1 n25 exit=$E2"