-------------------
leanCoP-SInE (v2.1)

Jens Otten, Thomas Raths
University of Potsdam


-----------
Description

leanCoP-SInE is an automated theorem prover for classical first-
order logic. It combines the systems SInE 0.4 and leanCoP 2.1.

SInE is an axiom selection system for first-order theories. It
uses a syntactic approach based on symbols' presence in axioms
and the conjecture. SInE is developed by Krystof Hoder. See also
http://www.cs.man.ac.uk/~hoderk/sine.

leanCoP is a compact theorem prover for classical first-order
logic implemented in Prolog. See http://www.leancop.de for more
details.

------------
Installation

A Prolog system and Python are required to run leanCoP-SInE.
Set the path for the Prolog system (either ECLiPSe, SICStus
or SWI) and the path for the leanCoP-SInE prover in the file
leancop_sine.sh. This file also includes parameters to control
the output of the proof and to specify the proof layout.

---------
Execution

The command to run the prover is
./sine_batch.py -e leancop -t <time limit>  <batch file>

A parameter -p <path> can be added to specify the base for relative
paths to axiom files specified in include() statements. When not
specified, the TPTP environment variable or the current directory
is used. See below for a batch file example.

The string output for a theorem is:
# SZS status Theorem

The string output for running out of some limited resource is:
# Cannot determine problem status within resource limit

------------------
Example batch file

% SZS start BatchIncludes
include('Axioms/AGT001+0.ax').
include('Axioms/AGT001+1.ax').
include('Axioms/NUM005+0.ax').
include('Axioms/NUM005+1.ax').
% SZS end BatchIncludes
% SZS start BatchProblems
/TPTP/Problems/AGT/AGT001+1.p proof_output_file_1
/TPTP/Problems/AGT/AGT002+1.p proof_output_file_2
/TPTP/Problems/AGT/AGT003+1.p proof_output_file_3
% SZS end BatchProblems