1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
System Details
--------------
ATP system name : E 0.32 "Lingia"
TPTP version : v2.2.0
tptp2X flags : -f setheo:sign -t rm_equality:rstfp
CPU : SUN Ultra-60, 300 MHz UltraSPARC II
RAM size : 384 MB
Operating system : Solaris 2.6
Implementation : ANSI C. Compiler: gcc version egcs-2.90.23 980102
(egcs-1.0.1 release).
Compiler options: -O3 -Wall -Wno-char-subscripts
-Wshadow -ansi -pedantic (+package-specific
defines)
Resource limits : 400 seconds, 192 MB
Settings/flags : -xAuto (Automatic selection of search heuristic
and strategy)
-s (Minimal output)
--print-pid (for technical reasons)
--resources-info (for technical reasons)
--memory-limit=192
--cpu-limit=400
Results format : Name State Time Reason
Name: File name of the problem (as generated by
tptp2X),
State: T - Theorem (unsatisfiable)
N - No theorem (satisfiable)
F - Failure
Time: CPU time in seconds
Reason: maxtime - No solution within time
limit
maxmem - Prover ran out of memory
success - Success
incomplete - Prover discarded clauses due
to lack of memory, remaining
system is saturated
unknown - Unknown (Bug or other
problem)
Results values : See above
Comments : Tested on CNF problems only.
: The prover should be complete in this
configuration unless it runs low on memory (even
in this case it seems to be practically
complete, i.e. the incompletness did never
manifest in any of our test runs). It did not
make use of clause type information.
Submitted by : Stephan Schulz (schulz@informatik.tu-muenchen.de)
|
