-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmodel
78 lines (78 loc) · 3.45 KB
/
model
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
c PicoSAT SAT Solver Version 960
c Copyright (c) 2006 - 2014 Armin Biere JKU Linz
c gcc -Wall -Wextra -DNDEBUG -O3
c
c using 2 as default phase
c
c parsing infile.cnf
c parsed header 'p cnf 494 5304'
c initialized 494 variables
c found 5304 non trivial clauses
c
c random number generator seed 0
c
c seconds variables original learned agility
c level used conflicts limit MB
c
c s 0.0 0.0 431 24.1 4390 0 37 0 0.0 0.3
c
c initial reduction limit 1000 clauses
c
c + 0.0 47.8 428 40.1 4390 100 133 1100 5.0 0.4
c R 0.0 48.8 428 41.1 4390 107 140 1100 5.3 0.4
c 1 0.0 61.6 422 71.5 4390 219 248 1100 8.6 0.4
c
c seconds variables original learned agility
c level used conflicts limit MB
c
s SATISFIABLE
v -1 -2 3 4 5 6 -7 8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 20 21 22 23 -24
v -25 -26 27 -28 -29 -30 -31 32 -33 34 35 36 37 38 -39 -40 -41 42 43 -44 -45
v -46 -47 -48 -49 -50 51 -52 -53 54 -55 -56 57 -58 -59 60 -61 62 -63 -64 65 -66
v 67 68 -69 -70 71 -72 73 74 -75 -76 -77 78 79 -80 -81 -82 -83 -84 -85 -86 87
v -88 89 -90 91 -92 -93 -94 -95 96 97 -98 -99 -100 -101 -102 -103 -104 -105 106
v 107 108 -109 -110 111 -112 113 -114 -115 116 -117 -118 -119 120 -121 122 -123
v -124 125 -126 127 128 -129 -130 -131 132 133 -134 135 136 -137 -138 -139 -140
v -141 -142 -143 144 145 -146 147 148 149 -150 -151 152 -153 -154 155 -156 -157
v 158 -159 -160 -161 162 -163 164 -165 -166 -167 -168 -169 -170 -171 -172 173
v -174 -175 176 -177 178 -179 180 -181 -182 183 -184 185 -186 -187 -188 -189
v -190 -191 -192 -193 -194 195 196 197 -198 199 -200 201 -202 203 -204 205 -206
v 207 -208 -209 210 -211 -212 -213 -214 -215 -216 -217 218 -219 -220 221 222
v -223 -224 225 -226 -227 228 -229 230 -231 -232 -233 -234 -235 -236 -237 238
v -239 -240 -241 -242 243 244 -245 246 247 -248 -249 -250 -251 252 -253 -254
v 255 -256 257 258 -259 -260 -261 262 -263 -264 -265 -266 267 268 -269 -270
v -271 272 273 -274 -275 -276 -277 -278 -279 280 -281 -282 -283 -284 -285 286
v -287 -288 -289 -290 -291 -292 -293 294 -295 296 -297 298 -299 -300 -301 -302
v -303 -304 -305 -306 307 -308 309 310 311 -312 313 314 315 -316 317 318 -319
v -320 321 322 323 324 -325 -326 327 -328 329 -330 -331 -332 333 -334 -335 -336
v -337 -338 339 -340 -341 -342 -343 -344 -345 346 -347 -348 349 -350 351 352
v 353 354 -355 -356 357 -358 -359 -360 361 -362 -363 364 365 366 -367 -368 -369
v 370 371 -372 -373 374 -375 -376 -377 -378 379 -380 381 382 -383 384 -385 -386
v 387 -388 389 -390 -391 392 -393 -394 395 -396 -397 398 399 400 401 -402 403
v 404 405 -406 -407 -408 -409 -410 -411 -412 413 414 -415 416 417 418 -419 -420
v -421 -422 -423 -424 -425 -426 427 428 429 -430 431 432 -433 -434 435 436 437
v 438 -439 -440 441 -442 -443 -444 -445 -446 -447 448 -449 -450 -451 -452 453
v 454 455 -456 457 -458 459 -460 461 -462 -463 464 465 -466 467 468 -469 -470
v 471 -472 473 -474 -475 476 -477 478 -479 -480 -481 482 -483 -484 -485 -486
v -487 -488 489 -490 491 -492 -493 -494 0
c
c 4 iterations
c 2 restarts
c 0 failed literals
c 219 conflicts
c 1167 decisions
c 72 fixed variables
c 2547 learned literals
c 4.3% deleted literals
c 6450 propagations
c 54830 visits
c 71.5% variables used
c 0.0 seconds in library
c 0.4 megaprops/second
c 3.1 megavisits/second
c probing 0.0 seconds 3%
c 1 simplifications
c 0 reductions
c 0.0 MB recycled
c 0.4 MB maximally allocated
c 0.0 seconds total run time