iprover/README.CASC-J6 at master · edechter/iprover · GitHub

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

Install:
========
1) OCaml >= 3.12

2)
./configure
make

Run:
=====

1) iproveropt_run.sh time_limit problem_name


2) for FNT and other satisfiability divisions:

   iproveropt_run_sat.sh time_limit problem_name


3) LTB.

 LTB Turing:
------------

   iprover_path/LTB/iprover_sine.sh iprover_path/iproveropt iprover_path/VClausifier/vclausify_rel overall_time_limit LTB.batch


 General LTB:
---------------
   iprover_path/LTB/iprover_sine.sh iprover_path/iproveropt iprover_path/VClausifier/vclausify_rel 0 LTB.batch

 *iProver-Eq*
  For iProver-Eq LTB in above replace  iprover_path/iproveropt with
  iprover_path_eq_path/iprover-cvc-eq-nc


Status strings:
========================

% SZS status Theorem
% SZS status Unsatisfiable
% SZS status CounterSatisfiable
% SZS status Satisfiable

% SZS status Unknown

Proof output:
=============
% SZS output start CNFRefutation
...
% SZS output end CNFRefutation

Answer output:
=============

% SZS answers Tuple ...

Model outputs (2 types):
===============
% SZS output start Model
...
% SZS output end Model

% SZS output start Saturation
...
% SZS output end Saturation