SAT-Inspired Higher-Order Eliminations

This is the package containing the raw evaluation data for the paper "SAT-Inspired Higher-Order Eliminations" by Jasmin Blanchette and Petar Vukmirović.

The problems used for the evaluation are located in the "problems" directory. The five categories are

    tptp_th0 (called T0 in Fig. 1 of the paper),
    tptp_th1 (called T1 in Fig. 1),
    seventeen_th0 (called S0 in Fig. 1)
    seventeen_th1 (called S1 in Fig. 1)
    tptp_cnffof (called F in Fig. 1)

The empirical results are located in the "results" directory, under the following names, corresponding to the category names above:

    tptp_th0_results.csv
    tptp_th1_results.csv
    seventeen_th0_results.csv
    seventeen_th1_results.csv
    tptp_cnffof_results.csv

The CSV files were produced by StarExec. Each nonheader row gives the prover's performance on one problem. For example, the row

    74437543,Problems/AGT/AGT036^1.p,2900058,Zipperposition---2.2pre-hoelim-v2,2410,hlbe-in,92437,complete,2.09374,0.983524,1684480.0,Theorem,Theorem,THM-Ref,Ref,THM

in "tptp_th0_results.csv" indicates that the HLBE inprocessing mode of Zipperposition ("hlbe-in") was able to prove the TPTP problem "AGT036^1.p", as indicated by the "THM" result in the last column. "THM" and "UNS" (unsatisfiable) correspond to a successful proof; other outcomes are considered failures.

Figure 1 was generated using the script "script/gen_figure.py", which must be run from the "script" directory.

The "binaries" directory contains the StarExec package used to run the evaluation. The package is called "bin" in accordance with StarExec conventions. Inside it, "zipperposition" and "eprover-ho" are the 64-bit Linux binaries for the Zipperposition prover and its E backend, and the other files are scripts used to run various configurations in time slices. When running the scripts locally, set the environment variables "STAREXEC_CPU_LIMIT" and "STAREXEC_WALLCLOCK_LIMIT" to suitable time limits in seconds.

Zipperposition was compiled from the repositiory version with the git commit hash 2a66166453ac32c0 on the "wip_ho_elimination_techniques" branch. E was compiled with the "--enable-ho" configuration option from an unspecified repository version. The Zipperposition and E repositories are available online (https://github.com/sneeuwballen/zipperposition and https://github.com/eprover/eprover)