eground

EGROUND(1)                       User Commands                      EGROUND(1)



NAME
       eground - manual page for eground 1.9

SYNOPSIS
       eground [options] [files]

DESCRIPTION
       eground 1.9

       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.

       Options

       -h

       --help

              Print a short description of program usage and options.

       --version

              Print the version number of the program.

       -v

       --verbose[=<arg>]

              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 <arg>

       --output-file=<arg>

              Redirect output into the named file.

       -s

       --silent

              Equivalent to --output-level=0.

       -l <arg>

       --output-level=<arg>

              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-2 format instead of E-LOP (except includes, which are
              handles as in TPTP-3, as TPTP-2 include syntax is considered
              harmful).

       --tptp-out

              Print TPTP-2 format instead of E-LOP.

       --tptp-format

              Equivalent to --tptp-in and --tptp-out.

       --tptp2-in

              Synonymous with --tptp-in.

       --tptp2-out

              Synonymous with --tptp-out.

       --tptp2-format

              Synonymous with --tptp-format.

       --tstp-in

              Parse TPTP-3 format instead of E-LOP (Note that TPTP-3 syntax is
              still under development, and the version implemented may not be
              fully conformant at all times. It works on all TPTP 3.0.1 input
              files (including includes).

       --tstp-out

              Print output clauses in TPTP-3 syntax.

       --tstp-format

              Equivalent to --tstp-in and --tstp-out.

       --tptp3-in

              Synonymous with --tstp-in.

       --tptp3-out

              Synonymous with --tstp-out.

       --tptp3-format

              Synonymous with --tstp-format.

       -d

       --dimacs

              Print output in the DIMACS format suitable for many
              propositional provers.

       --split-tries[=<arg>]

              Determine the number of tries for splitting. If 0, no splitting
              is performed. If 1, only variable-disjoint splits are done.
              Otherwise, up to the desired number of variable permutations is
              tried to find a splitting subset. The option without the
              optional argument is equivalent to --split-tries=1.

       -U

       --no-unit-subsumption

              Do not check if clauses are subsumed by previously encountered
              unit 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 <arg>

       --memory-limit=<arg>

              Limit the memory the system 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[=<arg>]

              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[=<arg>]

              Limit the cpu time spend in grounding. After the time expires,
              the prover will print an partial system. The option without the
              optional argument is equivalent to --soft-cpu-limit=310.

       -i

       --add-one-instance

              If the grounding procedure runs out of time or memory, try to
              add at least one instance of each clause to the set. This might
              fail for  really large clause sets, since the reserve memory
              kept for this purpose may be insufficient.

       -g <arg>

       --give-up=<arg>

              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 yet
              implemented!  Note to self: Split clauses need to get fresh
              variables if this is to work!

       -M

       --fix-minisat

              Fix the preamble to include only the maximum variable index, to
              compensate for MiniSAT's problematic interpretation of the DIMAC
              syntax.

REPORTING BUGS
       Report bugs to <schulz@eprover.org>. Please include the following, if
       possible:

       * The version of the package as reported by eprover --version.

       * The operating system and version.

       * The exact command line that leads to the unexpected behaviour.

       * A description of what you expected and what actually happend.

       * If possible all input files necessary to reproduce the bug.

COPYRIGHT
       Copyright 1998-2014 by Stephan Schulz, schulz@eprover.org

       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://www.eprover.org

       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 DHBW Stuttgart Fakultaet Technik Informatik
       Rotebuehlplatz 41 70178 Stuttgart Germany



eground 1.9                        July 2015                        EGROUND(1)