PyRes is a theorem prover for full first-order logic with equality. It is written in very clear and extensively documented Python 3, with the aim of illustrating the basic design and implementation of a theorem prover build on the currently predominant saturation paradigm. You can directly browse the source code on GitHub at https://github.com/eprover/PyRes.

Below is the supporting data for our paper Teaching Automated Theorem Proving by Example: PyRes 1.2.

1. •PyRes1.2_DATA.tgz contains the detailed records of the performance data in the paper.
   

2. •PyRes1.2.tgz  contains the source distribution (including StarExec Miami runscripts).
   

3. •PyRes1.2.zip is an StarExec package of PyRes 1.2, including all runscripts used for the paper.