SAT-Inspired Higher-Order Eliminations

<p>This is the package containing the raw evaluation data for the paper &quot;SAT-Inspired Higher-Order Eliminations&quot; by Jasmin Blanchette and Petar Vukmirović.</p> <p>The problems used for the evaluation are located in the &quot;problems&quot; directory. The seven categories are</p> <p>&nbsp; &nbsp; seventeen_th0 (called S0 in Fig. 1 of the paper)<br> &nbsp; &nbsp; seventeen_th1 (called S1 in Fig. 1)<br> &nbsp; &nbsp; tptp_th0 (called TH0 in Fig. 1)<br> &nbsp; &nbsp; tptp_th1 (called TH1 in Fig. 1)<br> &nbsp; &nbsp; tptp_cnffof (called CF in Fig. 1)<br> &nbsp; &nbsp; tptp_tf0 (called TF0 in Fig. 1)<br> &nbsp; &nbsp; tptp_tf1 (called TF1 in Fig. 1)</p> <p>The empirical results are located in the &quot;results&quot; directory, under the following names, corresponding to the category names above:</p> <p>&nbsp; &nbsp; seventeen_th0_results.csv<br> &nbsp; &nbsp; seventeen_th1_results.csv<br> &nbsp; &nbsp; tptp_th0_results.csv<br> &nbsp; &nbsp; tptp_th1_results.csv<br> &nbsp; &nbsp; tptp_cnffof_results.csv<br> &nbsp; &nbsp; tptp_tf0_results.csv<br> &nbsp; &nbsp; tptp_tf1_results.csv</p> <p>The CSV files were produced by StarExec. Each nonheader row gives the prover&#39;s performance on one problem. For example, the row</p> <p>&nbsp; &nbsp; 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</p> <p>in &quot;tptp_th0_results.csv&quot; indicates that the HLBE inprocessing mode of Zipperposition (&quot;hlbe-in&quot;) was able to prove the TPTP problem &quot;AGT036^1.p&quot;, as indicated by the &quot;THM&quot; result in the last column. &quot;THM&quot; and &quot;UNS&quot; (unsatisfiable) correspond to a successful proof; other outcomes are considered failures.</p> <p>Figure 1 was generated using the script &quot;script/gen_figure.py&quot;, which must be run from within the &quot;script&quot; directory.</p> <p>The &quot;binaries&quot; directory contains the StarExec package used to run the evaluation. The package is called &quot;bin&quot; in accordance with StarExec conventions. Inside it, &quot;zipperposition&quot; and &quot;eprover-ho&quot; 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 &quot;STAREXEC_CPU_LIMIT&quot; and &quot;STAREXEC_WALLCLOCK_LIMIT&quot; to suitable time limits in seconds.</p> <p>Zipperposition was compiled from the repositiory version with the git commit hash 2a66166453ac32c0 on the &quot;wip_ho_elimination_techniques&quot; branch. E was compiled with the &quot;--enable-ho&quot; 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).</p>