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:
[e-mail]: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.