This code implements simple, resolution-based theorem provers for
first-order logic. It is released as free software under the GNU GPL
version 2, and without any warranty. See the file COPYING for
details and the individual source headers for copyright information.

Installation:
=============

Just clone the repository into a new directory, with e.g.
git clone https://github.com/eprover/PyRes.git

No futher installation should be necessary. If you are on a UNIX-like
OS (including Linux or macOS/OS-X), and "python3" is not in your
standard search path (or not Python 3), you may need to edit the
#!-line at the beginning of the three main programs (see below),
or in all modules if you want to run the unit tests.


pyres-simple.py
===============

This is the simplest example of a prover for the clausal fragment of
first-order logic. It implements the basic given-clause loop with
first-in-first-out clause selection and without any redundancy
elimination.

Suggested command line:
./pyres-simple.py EXAMPLES/PUZ002-1.p

PUZ001-1.p is quite hard for pyres-simple!


pyres-cnf.py
===========

This version of the prover processes the same logic as
pyres-simple.py, but adds some performance-enhancing features. This
include better clause selection heuristics, subsumption, and negative
literal selection.

Suggested command line:
./pyres-cnf.py -tfb -HPickGiven5 -nsmallest EXAMPLES/PUZ001-1.p

pyres-fof.py
===========

This prover adds a simple clausifier, so it is able to process full
first-order logic. It also will detect the use of equality, and add
equality axioms. Otherwise, it is similar to pyres-cnf.py.


Suggested command line:
./pyres-fof.py -tifbp -HPickGiven5 -nlargest EXAMPLES/PUZ001+1.p



======== Information for CASC =================

The system comes as a zip file in StarExec compatible format. It
requires (any) Python3 as python3. The StarExec package can be
regenerated by "make starexec". THIS WILL OVERWRITE
$(HOME)/StarExec WITHOUT FURTHER WARNING. You can change the build
path in the Makefile.


The runscript is starexec_run_PyRes_default

Problem is CNF and unsatisfiable:

# SZS status Unsatisfiable

Problem is CNF and satisfiable:

# SZS status Satisfiable

Problem is FOF and a theorem:

# SZS status Theorem

Problem is FOF and not a theorem:

# SZS status CounterSatisfiable

The start of solution output for proofs:

# SZS output start CNFRefutation.

The end of solution output for proofs:

# SZS output end CNFRefutation.

The start of solution output for models/saturations:

# SZS output start Saturation.

The end of solution output for models/saturations:

# SZS output end Saturation.