Seventeen provers under the hammer

This archive contains used benchmarks, raw results, scripts to create tables from the paper, and the provers used for all experiments in the the paper Seventeen provers under the hammer. The benchmarks used in the experiments are separated by the table in which they are used: Table Archive 4 baseline_probs.zip 6 max_facts_probs.zip 7 lam_trans_probs.zip 8 poly_enc_probs.zip 9 mono_enc_probs.zip Note that there are 5000 benchmarks in each subclass of benchmarks. The raw results are stored in results.zip archive. This archive contains JobInfo files from StarExec, our evaluation environment. JobInfo files are separated per experiment, with self explanatory directory structure. Each of these archives contains a single .csv file in in which each row describes one run of a prover on one benchmark and contains information such as the used CPU time and memory resources, if the prover solved the problem and path to the benchmark. All the tables in the paper that contain evaluation results are automatically created using scripts from table_scripts. To create the tables, first extract the archives results.zip and table_scripts.zip. Assuming they have been extracted to directories results/ and table_scripts/, respectively, the following commands create the tables: Table Generation command 4 python3 table_scripts/get_table.py results/baseline table_scripts/baseline.json 5 python3 table_scripts/get_table.py results/ table_scripts/running_time.json --no-column-best --no-row-best 6 python3 table_scripts/get_table.py results/ table_scripts/max_facts.json 7 python3 table_scripts/get_table.py results/ table_scripts/lam_trans.json 8 python3 table_scripts/get_table.py results/ table_scripts/poly_enc.json 9 python3 table_scripts/get_table.py results/ table_scripts/mono_enc.json 10 python3 table_scripts/get_greedy_seq.py results/ table_scripts/greedy.json --max-configurations 16 All provers, except for ENIGMA (which has several gigabyte installation) are stored in provers.zip. Note that due to library dependencies, and that they are packaged in StarExec-specific way, the best way to install them is by reuploading them to StarExec. ENIGMA is available at this link