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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
This is the required ReadMe file for the CASC competitions.
-----------------------------------------------------------
For installation, follow the instructions in the main README
file. Make sure to do a proper install, so that e_ltb_runner can find
the executables. If you need to rebuild a StarExec version
from the sources, run "make starexec", which should take care of
everything. Note that THIS WILL DELETE $(STAREXECPATH), which
is by default define as $(HOME)/StarExec. Edit Makefile.vars
to choose a different directory for building the StarExec
distribution.
The strategies for the different divisions are:
FOF UEQ: starexec_run_E---_autoschedule
FNT EPR: starexec_run_E---_satautoschedule
LTB: starexec_run_E---LTB28
Distinguished strings for the results:
Problem is CNF and unsatisfiable:
# SZS status Unsatisfiable
Problem is CNF and satisfiable:
# SZS status Satisfiable
Problem is FOF and a theorem:
# SZS status Theorem
or
# SZS status ContradictoryAxioms
Problem is FOF and not a theorem:
# SZS status CounterSatisfiable
System gave up (usually resource limit)
# Failure:
The start of solution output for proofs:
# SZS output start CNFRefutation.
The end of solution output for proofs:
# SZS output end CNFRefutation.
The start of solution output for models/saturations:
# SZS output start Saturation.
The end of solution output for models/saturations:
# SZS output end Saturation.
LTB Problem processing:
# SZS status Started for <name>
# SZS status Ended for <name>
|
