1EGROUND(1)                       User Commands                      EGROUND(1)
2
3
4

NAME

6       eground - manual page for eground 2.6-DEBUG
7

SYNOPSIS

9       eground [options] [files]
10

DESCRIPTION

12       eground 2.6-DEBUG
13
14       Read  a set of clauses and determine if it can be grounded (i.e. is ei‐
15       ther 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
20       Options
21
22       -h
23
24       --help
25
26              Print a short description of program usage and options.
27
28       --version
29
30              Print the version number of the program.
31
32       -v
33
34       --verbose[=<arg>]
35
36              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
40       -o <arg>
41
42       --output-file=<arg>
43
44              Redirect output into the named file.
45
46       -s
47
48       --silent
49
50              Equivalent to --output-level=0.
51
52       -l <arg>
53
54       --output-level=<arg>
55
56              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
61       --print-statistics
62
63              Print a short statistical summary of clauses read and generated.
64
65       -R
66
67       --resources-info
68
69              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
74       --suppress-result
75
76              Supress actual printing of the result, just give a short message
77              about success. Useful mainly for test runs.
78
79       --lop-in
80
81              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
87       --tptp-in
88
89              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
93       --tptp-out
94
95              Print TPTP-2 format instead of E-LOP.
96
97       --tptp-format
98
99              Equivalent to --tptp-in and --tptp-out.
100
101       --tptp2-in
102
103              Synonymous with --tptp-in.
104
105       --tptp2-out
106
107              Synonymous with --tptp-out.
108
109       --tptp2-format
110
111              Synonymous with --tptp-format.
112
113       --tstp-in
114
115              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
120       --tstp-out
121
122              Print output clauses in TPTP-3 syntax.
123
124       --tstp-format
125
126              Equivalent to --tstp-in and --tstp-out.
127
128       --tptp3-in
129
130              Synonymous with --tstp-in.
131
132       --tptp3-out
133
134              Synonymous with --tstp-out.
135
136       --tptp3-format
137
138              Synonymous with --tstp-format.
139
140       -d
141
142       --dimacs
143
144              Print  output  in  the  DIMACS format suitable for many proposi‐
145              tional provers.
146
147       --definitional-cnf[=<arg>]
148
149              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
156       --old-cnf[=<arg>]
157
158              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 eq‐
162              uisatisfiable)  clause  normal forms. The option without the op‐
163              tional argument is equivalent to --old-cnf=24.
164
165       --miniscope-limit[=<arg>]
166
167              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
172       --split-tries[=<arg>]
173
174              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  op‐
178              tional argument is equivalent to --split-tries=1.
179
180       -U
181
182       --no-unit-subsumption
183
184              Do  not  check if clauses are subsumed by previously encountered
185              unit clauses.
186
187       -r
188
189       --no-unit-resolution
190
191              Do not perform forward-unit-resolution on new clauses.
192
193       -t
194
195       --no-tautology-detection
196
197              Do not perform tautology deletion on new clauses.
198
199       -m <arg>
200
201       --memory-limit=<arg>
202
203              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 So‐
207              laris and GNU/Linux.
208
209       --cpu-limit[=<arg>]
210
211              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
221       --soft-cpu-limit[=<arg>]
222
223              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
227       -i
228
229       --add-one-instance
230
231              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
236       -g <arg>
237
238       --give-up=<arg>
239
240              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 es‐
245              timated total number of clauses would  exceed  this  value  .  A
246              value of 0 will leave this test disabled.
247
248       -c
249
250       --constraints
251
252              Use  global purity constraints to restrict the number of instan‐
253              tiations done.
254
255       -C
256
257       --local-constraints
258
259              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
264       -M
265
266       --fix-minisat
267
268              Fix  the preamble to include only the maximum variable index, to
269              compensate for MiniSAT's problematic interpretation of the DIMAC
270              syntax.
271

REPORTING BUGS

273       Report  bugs  to <schulz@eprover.org>. Please include the following, if
274       possible:
275
276       * The version of the package as reported by eprover --version.
277
278       * The operating system and version.
279
280       * The exact command line that leads to the unexpected behaviour.
281
282       * A description of what you expected and what actually happend.
283
284       * If possible all input files necessary to reproduce the bug.
285
287       Copyright 1998-2021 by Stephan Schulz, schulz@eprover.org,  and  the  E
288       contributors (see DOC/CONTRIBUTORS).
289
290       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
294       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
299       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
304       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
310       The original copyright holder can be contacted via email or as
311
312       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
313       buehlplatz 41 70178 Stuttgart Germany
314
315
316
317eground 2.6-DEBUG                  July 2023                        EGROUND(1)
Impressum