eground 0.22dev Usage: eground [options] [files] Read a set of clauses and determine if it can be grounded (i.e. is either already ground or has no non-constant function symbols). If this is the case, print sufficiently many ground instances of the clauses to guarantee that a ground refutation can be found for unsatisfiable clause sets. -h --help Print a short description of program usage and options. --version Print the version number of the program. -v --verbose[=] Verbose comments on the progress of the program by printing technical information to stderr. The short form or the long form without the optional argument is equivalent to --verbose=1. -o --output-file= Redirect output into the named file. -s --silent Equivalent to --output-level=0. -l --output-level= Select an output level, greater values imply more verbose output. Level 0 produces nearly no output except for the final clauses, level 1 produces minimal additional output. Higher levels are without meaning in eground (I think). --print-statistics Print a short statistical summary of clauses read and generated. -R --resources-info Give some information about the resources used by the system. You will usually get CPU time information. On systems returning more information with the rusage() system call, you will also get information about memory consumption. --suppress-result Supress actual printing of the result, just give a short message about success. Useful mainly for test runs. --tptp-in Parse TPTP format instead of lop (does not understand includes, as TPTP include syntax is considered harmful). --tptp-out Print TPTP format instead of lop. Implies --eqn-no-infix and will ignore --full-equational-rep. --tptp-format Equivalent to --tptp-in and --tptp-out. -d --dimacs Print output in the DIMACS format suitable for many propositional provers. --split-method= Determine how to treat ground literals in splitting. The argument is either '0' to denote no splitting of ground literals (they are all assigned to the first split clause produced), '1' to denote that all ground literals should form a single new clause, or '2', in which case ground literals are treated as usual and are all split off into individual clauses. By default, no splitting is as performed at all. -U --no-unit-subsumption Do not check if clauses are subsumed by previously encounteredunit clauses. -r --no-unit-resolution Do not perform forward-unit-resolution on new clauses. -t --no-tautology-detection Do not perform tautology deletion on new clauses. -m --memory-limit= Limit the memory the prover may use. The argument is the allowed amount of memory in MB. This option may not work everywhere, due to broken and/or strange behaviour of setrlimit() in some UNIX implementations. It does work under all tested versions of Solaris and GNU/Linux. --cpu-limit[=] Limit the cpu time the program should run. The optional argument is the CPU time in seconds. The program will terminate immediately after reaching the time limit, regardless of internal state. This option may not work everywhere, due to broken and/or strange behaviour of setrlimit() in some UNIX implementations. It does work under all tested versions of Solaris, HP-UX and GNU/Linux. As a side effect, this option will inhibit core file writing. The option without the optional argument is equivalent to --cpu-limit=300. --soft-cpu-limit[=] Limit the cpu time spend in grounding. After the time expires,the prover will print an partial system. This option is not yet supported! The option without the optional argument is equivalent to --soft-cpu-limit=310. -g --give-up= Give up early if the problem is unlikely to be reasonably small. If run without constraints, the programm will give up if the clause with the largest number of instances will be expanded into more than this number of instances. If run with contraints, the program keeps a running count and will terminate if the estimated total number of clauses would exceed this value . A value of 0 will leave this test disabled. -c --constraints Use global purity constraints to restrict the number of instantiations done. -C --local-constraints Use local purity constraints to further restrict the number of instantiations done. Implies the previous option. Not yetimplemented! Copyright 1998-2001 by Stephan Schulz, schulz@informatik.tu-muenchen.de This program is a part of the support structure for the E equational theorem prover. You can find the latest version of the E distribution as well as additional information at http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program (it should be contained in the top level directory of the distribution in the file COPYING); if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA The original copyright holder can be contacted as Stephan Schulz Technische Universitaet Muenchen Fakultaet fuer Informatik Arcisstrasse 20 D-80290 Muenchen Germany