THE LEO-II System Installation Guide
(Christoph Benzmueller and Nik Sultana)


NOTES:
  * LEO-II runs under OCaml
  * It follows the TPTP ATP System Building Conventions
     ( http://www.cs.miami.edu/~tptp/TPTP/Proposals/SystemBuild.html )


- LEO-II is designed to cooperate with first-order provers. Thus installation
  of a first order prover is crucial in order to run LEO-II. While LEO-II
  can cooperate with different first-order provers, we recommend here to
  install the 'The E Equational Theorem Prover' which is available at
  http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html

- In the following we assume that the binary for running prover E is available
  in file
                   [eprover-directory]/eprover
- In order to inform LEO-II where it can find this binary for E you need to
  provide a file
                   [your-homedirectory]/.leoatprc
  containing the following entries:
                   e = [eprover-directory]/eprover
		   epclextract = [eprover-directory]/epclextract

Running LEO-II in Automatic Mode:
- To start LEO-II you need to type:
                  [installation-directory]/leo2/bin/leo
- Parameters are given in the following sequence:
                  [installation-directory]/leo2/bin/leo [OPTIONS] [FILE]
  In order to see which options can be set, run
                  [installation-directory]/leo2/bin/leo --help
- Usage examples:
   [installation-directory]/leo2/bin/leo [installation-directory]/leo2/distrib_examples/BrownSmolka-1.thf --proofoutput 1

   [installation-directory]/leo2/bin/leo -d [installation-directory]/leo2/distrib_examples -f e -t 40
   (please make sure that you have write permissions for [installation-directory]/leo2/distrib_examples)

   At CASC LEO-II is called as follows:
   [installation-directory]/leo2/bin/leo --timeout 30 --proofoutput 1 --foatp e \
     --atp e=[e-directory]/eprover '[problem-file-directory/SET014^4.tptp'


Running LEO-II in Interactive Mode is not currently recommended due to several open issues.