-
Notifications
You must be signed in to change notification settings - Fork 1
/
b17-4r.qdimacs
123 lines (123 loc) · 1.22 KB
/
b17-4r.qdimacs
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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
c 2016-08-31 12:47:33 by qbfdd.py,v 1.2.2
c qbfdd.py /Users/markus/work/cadet/qbf-instances/tests/b17-4.qdimacs /Users/markus/work/cadet/cadet -m ddmin -g b
c
c mode: ddmin
c rounds: 1
c test runs: 1065
c time elapsed: 19.35s
c total: clauses : -0 (0.00%)
c variables: -7 (7.14%)
c literals : -37 (22.42%)
c
p cnf 91 109
a 11 12 13 14 15 16 17 18 0
e 1 2 3 4 5 6 7 8 9 10 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 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 0
-1 0
-2 0
-5 0
-9 0
-10 0
61 0
-62 0
63 0
-65 0
-44 0
-68 0
70 0
-71 0
72 0
-74 0
-76 0
79 0
80 0
81 0
-83 0
-86 0
-91 0
90 0
-89 0
90 0
88 0
3 0
87 0
87 0
85 0
84 0
84 0
82 0
-78 0
78 -77 0
78 -13 0
-14 77 0
75 0
75 0
75 0
73 0
-69 0
69 -67 0
69 -18 0
69 -17 0
-14 67 0
66 0
66 0
66 0
64 0
-60 0
-8 0
-7 0
-6 0
60 -4 0
60 -3 0
59 0
59 0
59 0
-55 0
59 0
59 0
59 0
58 0
57 0
56 0
54 0
53 0
52 0
51 0
50 0
49 0
48 0
47 0
46 0
45 0
-38 0
43 0
-42 0
13 -40 0
41 0
40 14 0
39 0
-31 0
-34 0
-37 0
13 -35 0
36 0
35 14 0
-2 0
16 -32 0
33 0
32 12 0
15 -29 0
30 0
29 11 0
-22 0
28 0
28 0
27 0
26 0
25 0
24 0
23 0
15 -20 0
21 0
20 11 0
19 0
19 0