CASC ReadMe

This file is a modified version of the regular 'install.txt' coming with 
E-KRHyper. The information here is concerning the operation of E-KRHyper 
in CASC only. 



   For CASC E-KRHyper accepts CNF and FOF input in TPTP-syntax.

   E-KRHyper is usually controlled with configuration files containing
   various flags and commands, and these files must be loaded into the prover
   together with the problem.
   For CASC this has been simplified: the user starts the shell script 
   'ekrhyper' (found in $INSTALLDIR/casc) with the problem file as its argument, 
   and the script then starts the prover and loads the the required files in the
   correct order. Thus the invocation is: 
   
   $INSTALLDIR/lib/ekrhyper/casc/ekrhyper %s
   
   where %s is the TPTP problem file, for example
   $INSTALLDIR/lib/ekrhyper/casc/ekrhyper ~/TPTP-v5.3.0/Problems/ALG/ALG011-1.p

   No other command line arguments are accepted. E-KRHyper will run until 
   it terminates on its own or is interrupted from the outside.
   
   (The 'ekrhyper' shell script corresponds to executing the following command:
   $INSTALLDIR/bin/ekrh $INSTALLDIR/lib/ekrhyper/casc/config.tme %s $INSTALLDIR/lib/ekrhyper/casc/run.tme)
   
   If E-KRHyper terminates, then the prover will print a line of SZS output to
   stdout:
   - for an unsatisfiable CNF/FOF problem:
   
    % SZS status Unsatisfiable
	
   - for a satisfiable CNF/FOF problem:

	% SZS status Satisfiable

   - for a FOF theorem:
	
	% SZS status Theorem
	
   - for a FOF problem with countersatisfiable conjecture:

	% SZS status CounterSatisfiable
	
Running E-KRHyper in CASC - LTB division:	

   In the LTB division E-KRHyper is run using the Perl script 'ekrhyper_ltb.pl'
   (found in $INSTALLDIR/casc). Please adjust the path variable $EKRHDIR in
   the script (line 10) to your installation, it should point to the same 
   directory as $INSTALLDIR.
   The command line invocation is:
   
   $INSTALLDIR/lib/ekrhyper/casc/ekrhyper_ltb.pl %s %d
   
   ...where %s is the name of a batch file and %d is the total time limit.
   
   If any file paths in the batch specification are not absolute, then 
   E-KRHyper will look for these in the directory specified by the $TPTP 
   environment variable.
   E-KRHyper will print the results for the individual problems into the output
   files specified in the batch file. An individual result is either one of the
   SZS output lines described above in section 4., or it is
   
   % SZS status GaveUp
   
   ...if E-KRHyper could not solve a particular problem and moved on to the next
   one.
   If the batch specification states that answer output is desired or required,
   then E-KRHyper will attempt to compute answers for the respective problems.
   If the prover succeeds in this, then the answer(s) will be printed in 
   addition to the normal SZS output stated above, using SZS Tuple Answer syntax.
   Example:
   
   % SZS status Theorem
   % SZS answers Tuple [[a,b,c],[d,e,f]].
   
   The script will also print its progress to stdout. For each problem it will print
   
   % SZS status Started for <problem>
   
   as soon as it has started working on <problem>.
   Once it has finished that problem, it will print the result (same as in the output
   file) to stdout, followed by
   
   % SZS status Ended for <problem>
   
   Example:
   % SZS status Started for Problems/CSR/CSR083+3.p
   % SZS status Theorem
   % SZS answers Tuple [[s__Human]].
   % SZS status Ended for Problems/CSR/CSR083+3.p