1EGROUND(1) User Commands EGROUND(1)
2
6 eground - manual page for eground 2.4-DEBUG
7
9 eground [options] [files]
10
12 eground 2.4-DEBUG
13 Read a set of clauses and determine if it can be grounded (i.e. is
15 either already ground or has no non-constant function symbols). If this
16 is the case, print sufficiently many ground instances of the clauses to
17 guarantee that a ground refutation can be found for unsatisfiable
18 clause sets.
19 Options
21 -h
23 --help
25 Print a short description of program usage and options.
27 --version
29 Print the version number of the program.
31 -v
33 --verbose[=<arg>]
35 Verbose comments on the progress of the program by printing
37 technical information to stderr. The short form or the long form
38 without the optional argument is equivalent to --verbose=1.
39 -o <arg>
41 --output-file=<arg>
43 Redirect output into the named file.
45 -s
47 --silent
49 Equivalent to --output-level=0.
51 -l <arg>
53 --output-level=<arg>
55 Select an output level, greater values imply more verbose out‐
57 put. Level 0 produces nearly no output except for the final
58 clauses, level 1 produces minimal additional output. Higher lev‐
59 els are without meaning in eground (I think).
60 --print-statistics
62 Print a short statistical summary of clauses read and generated.
64 -R
66 --resources-info
68 Give some information about the resources used by the system.
70 You will usually get CPU time information. On systems returning
71 more information with the rusage() system call, you will also
72 get information about memory consumption.
73 --suppress-result
75 Supress actual printing of the result, just give a short message
77 about success. Useful mainly for test runs.
78 --lop-in
80 Set E-LOP as the input format. If no input format is selected by
82 this or one of the following options, E will guess the input
83 format based on the first token. It will almost always correctly
84 recognize TPTP-3, but it may misidentify E-LOP files that use
85 TPTP meta-identifiers as logical symbols.
86 --tptp-in
88 Parse TPTP-2 format instead of E-LOP (except includes, which are
90 handles as in TPTP-3, as TPTP-2 include syntax is considered
91 harmful).
92 --tptp-out
94 Print TPTP-2 format instead of E-LOP.
96 --tptp-format
98 Equivalent to --tptp-in and --tptp-out.
100 --tptp2-in
102 Synonymous with --tptp-in.
104 --tptp2-out
106 Synonymous with --tptp-out.
108 --tptp2-format
110 Synonymous with --tptp-format.
112 --tstp-in
114 Parse TPTP-3 format instead of E-LOP (Note that TPTP-3 syntax is
116 still under development, and the version implemented may not be
117 fully conformant at all times. It works on all TPTP 3.0.1 input
118 files (including includes).
119 --tstp-out
121 Print output clauses in TPTP-3 syntax.
123 --tstp-format
125 Equivalent to --tstp-in and --tstp-out.
127 --tptp3-in
129 Synonymous with --tstp-in.
131 --tptp3-out
133 Synonymous with --tstp-out.
135 --tptp3-format
137 Synonymous with --tstp-format.
139 -d
141 --dimacs
143 Print output in the DIMACS format suitable for many proposi‐
145 tional provers.
146 --definitional-cnf[=<arg>]
148 Tune the clausification algorithm to introduces definitions for
150 subformulae to avoid exponential blow-up. The optional argument
151 is a fudge factor that determines when definitions are intro‐
152 duced. 0 disables definitions completely. The default works
153 well. The option without the optional argument is equivalent to
154 --definitional-cnf=24.
155 --old-cnf[=<arg>]
157 As the previous option, but use the classical, well-tested
159 clausification algorithm as opposed to the newewst one which
160 avoides some algorithmic pitfalls and hence works better on some
161 exotic formulae. The two may produce slightly different (but
162 equisatisfiable) clause normal forms. The option without the
163 optional argument is equivalent to --old-cnf=24.
164 --miniscope-limit[=<arg>]
166 Set the limit of variables to miniscope per input formula. The
168 build-in default is 1000. Only applies to the new (default)
169 clausification algorithm The option without the optional argu‐
170 ment is equivalent to --miniscope-limit=2147483648.
171 --split-tries[=<arg>]
173 Determine the number of tries for splitting. If 0, no splitting
175 is performed. If 1, only variable-disjoint splits are done. Oth‐
176 erwise, up to the desired number of variable permutations is
177 tried to find a splitting subset. The option without the
178 optional argument is equivalent to --split-tries=1.
179 -U
181 --no-unit-subsumption
183 Do not check if clauses are subsumed by previously encountered
185 unit clauses.
186 -r
188 --no-unit-resolution
190 Do not perform forward-unit-resolution on new clauses.
192 -t
194 --no-tautology-detection
196 Do not perform tautology deletion on new clauses.
198 -m <arg>
200 --memory-limit=<arg>
202 Limit the memory the system may use. The argument is the allowed
204 amount of memory in MB. This option may not work everywhere, due
205 to broken and/or strange behaviour of setrlimit() in some UNIX
206 implementations. It does work under all tested versions of
207 Solaris and GNU/Linux.
208 --cpu-limit[=<arg>]
210 Limit the cpu time the program should run. The optional argument
212 is the CPU time in seconds. The program will terminate immedi‐
213 ately after reaching the time limit, regardless of internal
214 state. This option may not work everywhere, due to broken and/or
215 strange behaviour of setrlimit() in some UNIX implementations.
216 It does work under all tested versions of Solaris, HP-UX and
217 GNU/Linux. As a side effect, this option will inhibit core file
218 writing. The option without the optional argument is equivalent
219 to --cpu-limit=300.
220 --soft-cpu-limit[=<arg>]
222 Limit the cpu time spend in grounding. After the time expires,
224 the prover will print an partial system. The option without the
225 optional argument is equivalent to --soft-cpu-limit=310.
226 -i
228 --add-one-instance
230 If the grounding procedure runs out of time or memory, try to
232 add at least one instance of each clause to the set. This might
233 fail for really large clause sets, since the reserve memory
234 kept for this purpose may be insufficient.
235 -g <arg>
237 --give-up=<arg>
239 Give up early if the problem is unlikely to be reasonably small.
241 If run without constraints, the programm will give up if the
242 clause with the largest number of instances will be expanded
243 into more than this number of instances. If run with contraints,
244 the program keeps a running count and will terminate if the
245 estimated total number of clauses would exceed this value . A
246 value of 0 will leave this test disabled.
247 -c
249 --constraints
251 Use global purity constraints to restrict the number of instan‐
253 tiations done.
254 -C
256 --local-constraints
258 Use local purity constraints to further restrict the number of
260 instantiations done. Implies the previous option. Not yet imple‐
261 mented! Note to self: Split clauses need to get fresh variables
262 if this is to work!
263 -M
265 --fix-minisat
267 Fix the preamble to include only the maximum variable index, to
269 compensate for MiniSAT's problematic interpretation of the DIMAC
270 syntax.
271
273 Report bugs to <schulz@eprover.org>. Please include the following, if
274 possible:
275 * The version of the package as reported by eprover --version.
277 * The operating system and version.
279 * The exact command line that leads to the unexpected behaviour.
281 * A description of what you expected and what actually happend.
283 * If possible all input files necessary to reproduce the bug.
285
287 Copyright 1998-2019 by Stephan Schulz, schulz@eprover.org, and the E
288 contributors (see DOC/CONTRIBUTORS).
289 This program is a part of the distribution of the equational theorem
291 prover E. You can find the latest version of the E distribution as well
292 as additional information at http://www.eprover.org
293 This program is free software; you can redistribute it and/or modify it
295 under the terms of the GNU General Public License as published by the
296 Free Software Foundation; either version 2 of the License, or (at your
297 option) any later version.
298 This program is distributed in the hope that it will be useful, but
300 WITHOUT ANY WARRANTY; without even the implied warranty of MER‐
301 CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
302 Public License for more details.
303 You should have received a copy of the GNU General Public License along
305 with this program (it should be contained in the top level directory of
306 the distribution in the file COPYING); if not, write to the Free Soft‐
307 ware Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
308 02111-1307 USA
309 The original copyright holder can be contacted via email or as
311 Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Rote‐
313 buehlplatz 41 70178 Stuttgart Germany
314eground 2.4-DEBUG January 2020 EGROUND(1)