GENERAL INFORMATION

1. Title of Dataset: SMT-Solving Induction Proofs of Inequalities Benchmarking Repository

2. Author Information
	A. Investigator Contact Information
		Name: Ali Kemal Uncu
		Institution: Australian Academy of Sciences
		Institution: University of Bath
		ORCID: 0000-0001-5631-6424

	B. Investigator Contact Information
		Name: James Davenport
		Institution: University of Bath
		ORCID: 0000-0002-3982-7545

	C. Investigator Contact Information
		Name: Matthew England
		Institution: Coventry University
		ORCID: 0000-0001-5729-3420


##############################
This repository contains the full list of files and the benchmarking results that were used in the benchmarking processes described in the paper:
A.K. Uncu, J.H. Davenport and M. England. "SMT-Solving Induction Proofs of Inequalities".  Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2022).  
The files are split in three branches. The Mathematica and Maple files include the calls that were made to the respective computer algebra systems, and the smt2 files are the ones used by the considered SMT solvers: Z3, CVC5 and Yices.
The Benchmarking Results cvc has the results.  The columns record the file names, the satisfiability outcome of the calls, then the times (in seconds) of the respective programmes. Any empty box (which the Maple:-RegularChains column has) would mean that the implementation does not accept that sort of input (this is due to rational functions - see the paper for details). Any time over 1200 seconds would mean that the program times out and the outcome of the question was not found in the given time.
##############################