Superposition with First-Class Booleans and Inprocessing Clausification

This archive contains the raw evaluation results and scripts for running the<br> experiments described in the article Superposition with First-Class Booleans<br> and Inprocessing Clausification and the associated technical report. Zipperposition is available at https://github.com/sneeuwballen/zipperposition. The configurations used in the evaluation are explained below and in the archive. The problems are stored in problems/ directory and divided in four<br> subdirectories, one for each category of the problem. Subdirectory Axioms/ holds<br> the axioms shared by TPTP problems. The subdirectory tptp-ho/ corresponds to<br> the benchmark set "TPTP Bool" of the paper. The results/ directory has subdirectories of the same name as the problems/<br> directory, each containting res.csv file with the raw evaluation results for the<br> given problem category. The result files are organized as follows: The columns give information about<br> the results of the experiment run for a given prover configuration (e.g., CPU<br> time, reported status, memory usage, etc.). Each row corresponds to one problem<br> file, whose name is given in the "prob_name" column. The "i_solver" column corresponds to a prover, whereas the "i_configuration"<br> column corresponds to a configuration, where i is a natural number identifying a<br> prover-configuration combination. Files ending with "summary.csv" contain concise summaries of evaluation runs for<br> a corresponding results file. Columns of these files are of the form<br> "{solver}_{configuration}", and rows contain different statistics described in<br> the "summary" column. Names of the solvers and configurations are self-explanatory, and follow the<br> nomenclature from the paper. Additionally, for Sledgehammer category of<br> benchmarks, there is additional set of configurations with names ending with<br> _tptp. Those configurations are the same as regular ones, but fix the input<br> syntax to TPTP. This is necessary since Sledgehammer files have no extensions. In the zipperposition/ directory you can find the scripts that run provided<br> Zipperposition binary (compiled only for Linux) on a given problem using a given<br> configuration. To run Zipperposition on a single problem using some<br> configuration use scripts with the name run_*.sh where * stands for the<br> configuration used in the evaluation. Configuration names match the ones used in<br> the result files. All scripts accept two arguments: 1) path to the problem 2) CPU timeout. For<br> example, to run problem with the path ~/problem.p using base configuration with<br> the time limit of 240 s execute ./run_base.sh ~/problem.p 240 Working installation of python3 and bash is required. Source code for Zipperposition can be obtained from the wip-bool-calculi branch<br> of Zipperposition git repository:<br> [e-mail]:sneeuwballen/zipperposition.git. The binary stored under scripts/<br> directory corresponds to compiled sources tagged with commit hash<br> b81ca9905c774212819afc004a6a17297fc070b6. Compilation instructions are as in<br> README.md file contained in the git repository.