Typed Superpostion

The benchmark files used are available here (download ca. 600MB / uncompressed ca. 8.8GB).

Pirate's output files are available here (119MB, uncompressed ca. 3.4GB) and SPASS's output file here (41MB, uncompress ca 2.4GB).

The files and outputs are sorted by type encoding and facts size. For SPASS's files the fact size has a suffix. A 'd' suffix stands for the default heuritics and an 'i' suffix for the heuristics tailored to Isabelle.

SupInd

The evaluation results and the benchmark files for the IsaPlanner and Clam benchmark are avaiable here.

A version of the SupInd Pirate including the necessary Scala 2.11 jars is available here. Note, that because the version used for evaluation had hard coded path and depended on a development version of Scala, this version has some changes to the version used for the evaluation.