Experimental Data on Relevance Filtering

Here you can download some of the data used for the experiments described in the paper "Lightweight Relevance Filtering for Machine-Generated Resolution Problems" by Paulson and Meng: specifically, the data for figures 15 to 17. The following items are available.

• unfiltered and filtered versions of the 285 problems
• tab-delimited files comparing the success rates (unfiltered against filtered) as processor time rises from 10 to 300 seconds, for three provers:
  • E
  • SPASS
  • Vampire