Superposition with First-Class Booleans and Inprocessing Clausification

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