Making Higher-Order Superposition Work

  • Petar Vukmirović (Creator)
  • Alexander Bentkamp (Creator)
  • Jasmin Christian Blanchette (Creator)
  • Simon Cruanes (Creator)
  • Visa Nummelin (Creator)
  • Sophie Tourret (Creator)



This package contains the raw evaluation data, and the scripts necessary for the reproduction of the results for the paper Making Higher-Order Superposition Work. Problems used for evaluation are available at

Zipperposition is available at See the README file in the archive below for detailed instructions on how to run it.

NOTE: The configuration named fig2_mc_av corresponds to the IC+AV configuration from the paper.

The name IC (immediate clausification) was introduces after the submission of the package to Zenodo.

Also, Figure 3, which contained the pseudocode, is removed in the camera-ready version of the paper.
Thus, all files figD_res(summary).csv with D >= 4 correspond to figures Figure D-1 in the paper. For example,
fig7_ressummary.csv corresponds to the figure 6 in the paper.

We are sorry for the inconvenience.
Date made available2021

Cite this