home | help 
EGROUND(1)			  User Commands 		      EGROUND(1)

NAME
     eground - manual page for eground 2.6

SYNOPSIS
     eground [options] [files]

DESCRIPTION
     eground 2.6

     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  techni-
	    cal  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  with-
	    out 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 in-
	    formation with the rusage() system call, you will also get	informa-
	    tion about memory consumption.

     --suppress-result

	    Supress  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-iden-
	    tifiers 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 harm-
	    ful).

     --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 sub-
	    formulae to avoid exponential blow-up. The optional  argument  is  a
	    fudge factor that determines when definitions are introduced. 0 dis-
	    ables  definitions	completely.  The  default works well. The option
	    without  the  optional   argument	is   equivalent   to   --defini-
	    tional-cnf=24.

     --old-cnf[=<arg>]

	    As the previous option, but use the classical, well-tested clausifi-
	    cation  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)  clausi-
	    fication  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 equiv-
	    alent 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 imple-
	    mentations. 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  af-
	    ter  reaching the time limit, regardless of internal state. This op-
	    tion 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 instantia-
	    tions done.

     -C

     --local-constraints

	    Use local purity constraints to further restrict the number  of  in-
	    stantiations 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 com-
	    pensate for MiniSAT's problematic interpretation of the  DIMAC  syn-
	    tax.

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

     * 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-2021 by Stephan Schulz, schulz@eprover.org, and the  E  con-
     tributors (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 addi-
     tional information at http://www.eprover.org

     This program is free software; you can redistribute it and/or modify it un-
     der 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  FIT-
     NESS 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 Foun-
     dation, 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  Rotebuehlplatz
     41 70178 Stuttgart Germany

eground 2.6			   August 2026			      EGROUND(1)
home | help