Provided by: eprover_3.2.0+ds-1_amd64 bug

NAME

       eground - manual page for eground 3.2.0

SYNOPSIS

       eground [options] [files]

DESCRIPTION

       eground 3.2.0

       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

              Suppress actual printing of the result, just give a short message about success. Useful mainly for
              test runs.

       --lop-in

              Set  E-LOP  as  the  input  format. If no input format is selected by this or one of the following
              options, E will guess the input format based on the first token. It will almost  always  correctly
              recognize  TPTP-3,  but  it  may misidentify E-LOP files that use TPTP meta-identifiers as logical
              symbols.

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

       --definitional-cnf[=<arg>]

              Tune  the  clausification algorithm to introduces definitions for subformulae to avoid exponential
              blow-up. The optional argument is a fudge factor that determines when definitions are  introduced.
              0  disables  definitions  completely.  The  default  works  well.  The option without the optional
              argument is equivalent to --definitional-cnf=24.

       --old-cnf[=<arg>]

              As the previous option, but use the classical, well-tested clausification algorithm as opposed  to
              the  newewst  one  which  avoides  some algorithmic pitfalls and hence works better on some exotic
              formulae. The two may produce slightly different (but equisatisfiable) clause  normal  forms.  The
              option without the optional argument is equivalent to --old-cnf=24.

       --miniscope-limit[=<arg>]

              Set  the  limit  of  variables  to miniscope per input formula. The build-in default is 1000. Only
              applies to the new (default) clausification algorithm The option without the optional argument  is
              equivalent to --miniscope-limit=2147483648.

       --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
              program 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 constraints, 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 happened.

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

COPYRIGHT

       Copyright 1998-2024 by Stephan Schulz, schulz@eprover.org, and the E contributors (see DOC/CONTRIBUTORS).

       This  program  is  a part of the distribution of the equational theorem prover E. 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 via email or as

       Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Lerchenstrasse 1 70174 Stuttgart Germany