Description of config file. --------------------------------------------- The first line of this file is the name of the theorem prover, for example Geo 2007F, Spass, Otter, E. This string is just like a comment. Nothing is done with it. The second line is a template according to which the names of the input files are created. For example "/home/nivelle/atp/inp". If th sixth line is set to 1, the inputs will be in files /home/nivelle/atp/inp0000, /home/nivelle/atp/inp0001, /home/nivelle/atp/inp0002. If the sixth line is set to 0, the inputs will all be in a single file that is reused after each call of theorem prover: /home/nivelle/atps/inp The third line has same format as second, but decribes output files template. The fourth line is a command with which the theorem prover should be called, e.g. home/nivelle/programs/geo2007f/geo -nonempty -tptp-input -inputfile %i > %o The following parameters can occur in the string: %i : name of input file. %t : time out. (if the prover can handle this) %o : name of output file. %n : replaced by newline \n. (so that multiple commands can be given in one string, e.g. when using tptp2X) The fifth line is the string with which proofs can be recognized. For example "END-OF-PROOF" in case of Geo. See System Information on CADE ATP System Competition webpage to get recognizing string of your favourite theorem prover. The sixth line is a flag. When set to one, different inputs are put in different files. The seventh line is also a flag. When set to zero, the prover is not run, and every goal is considered proven. This option is intended for a situation, where you want to generate the inputs to the prover, without running the prover (If you want to pass them to somebody who wants to try them on another prover). The eigth line is a string passed to the prover without change, if %t occurs in the command. It could be used for example for setting a timeout.