Satisfiable benchmark reported as unsatisfiable

[vuphan314]

ssat appears to report a zero satisfiability probability for a satisfiable benchmark.

d4p reports 0.820709 as the probability.

ssat reports 0.0:

ABC command line: "ssat s832a_15_7.sdimacs".

==== SSAT solving process ====

  > Setting (_upperLimit,_lowerLimit) to (-1,-1)
  > Use bdd as model counting engine
  > Start sat/unsat cube collection

[INFO] # of UNSAT cubes: 25
[INFO] # of   SAT cubes: 2016
[INFO] Exactly solve the instance: upper bound is tight

==== SSAT solving result ====

  > Upper bound = 0.000000e+00
  > Lower bound = 0.000000e+00
  > Time        =     0.18 sec

==== Runtime profiling ====

  > Time consumed on s1 solving  =     0.08 sec
  > Time consumed on s2 solving  =     0.01 sec
  > Time consumed on s2 greedy   =     0.01 sec
  > Time consumed on counting    =     0.00 sec
  > Time consumed on build  ckt  =     0.07 sec
  > Time consumed on strash ckt  =     0.00 sec
  > Time consumed on build  bdd  =     0.00 sec

==== Solving profiling ====

  > Number of s1 solving (SAT)          =       2016
  > Number of s1 solving (UNSAT)        =         25
  > Number of s2 solving                =       2042
  > Number of s2 successful greedy      =          0
  > Number of calls to model counting   =          1
  > Average length of learnt (base)     =   0.000000
  > Average length of learnt (subsume)  =   0.000000
  > Average length of learnt (partial)  =   0.000000
  > Average number of dropped literals  =   0.000000

Benchmark s832a_15_7.sdimacs:

p cnf 693 2017
r 0.52630084998192672163 1 0
r 0.45145173859870524335 2 0
r 0.83495322437974206498 3 0
r 0.41920503619210280899 4 0
r 0.98843744785517617668 5 0
r 0.26323313845700235802 6 0
r 0.43681107395014884265 7 0
r 0.08623731804172130033 8 0
r 0.21192652520292631912 9 0
r 0.20060022340739380731 10 0
r 0.91477328411715319589 11 0
r 0.20345975384353698345 12 0
r 0.06396060330772390667 13 0
r 0.74896047193349835069 14 0
r 0.75684804346402301256 15 0
r 0.56730550695077519574 16 0
r 0.44843752378555956639 17 0
r 0.76693948326429861595 18 0
r 0.13321462449488596924 19 0
r 0.35205296135790853373 20 0
r 0.76820904035949444388 21 0
r 0.07981500077462766463 22 0
r 0.00356466227469398600 23 0
e 24 0
e 25 0
e 26 0
e 27 0
e 28 0
e 29 0
e 30 0
e 31 0
e 32 0
e 33 0
e 34 0
e 35 0
e 36 0
e 37 0
e 38 0
e 39 0
e 40 0
e 41 0
e 42 0
e 43 0
e 44 0
e 45 0
e 46 0
e 47 0
e 48 0
e 49 0
e 50 0
e 51 0
e 52 0
e 53 0
e 54 0
e 55 0
e 56 0
e 57 0
e 58 0
e 59 0
e 60 0
e 61 0
e 62 0
e 63 0
e 64 0
e 65 0
e 66 0
e 67 0
e 68 0
e 69 0
e 70 0
e 71 0
e 72 0
e 73 0
e 74 0
e 75 0
e 76 0
e 77 0
e 78 0
e 79 0
e 80 0
e 81 0
e 82 0
e 83 0
e 84 0
e 85 0
e 86 0
e 87 0
e 88 0
e 89 0
e 90 0
e 91 0
e 92 0
e 93 0
e 94 0
e 95 0
e 96 0
e 97 0
e 98 0
e 99 0
e 100 0
e 101 0
e 102 0
e 103 0
e 104 0
e 105 0
e 106 0
e 107 0
e 108 0
e 109 0
e 110 0
e 111 0
e 112 0
e 113 0
e 114 0
e 115 0
e 116 0
e 117 0
e 118 0
e 119 0
e 120 0
e 121 0
e 122 0
e 123 0
e 124 0
e 125 0
e 126 0
e 127 0
e 128 0
e 129 0
e 130 0
e 131 0
e 132 0
e 133 0
e 134 0
e 135 0
e 136 0
e 137 0
e 138 0
e 139 0
e 140 0
e 141 0
e 142 0
e 143 0
e 144 0
e 145 0
e 146 0
e 147 0
e 148 0
e 149 0
e 150 0
e 151 0
e 152 0
e 153 0
e 154 0
e 155 0
e 156 0
e 157 0
e 158 0
e 159 0
e 160 0
e 161 0
e 162 0
e 163 0
e 164 0
e 165 0
e 166 0
e 167 0
e 168 0
e 169 0
e 170 0
e 171 0
e 172 0
e 173 0
e 174 0
e 175 0
e 176 0
e 177 0
e 178 0
e 179 0
e 180 0
e 181 0
e 182 0
e 183 0
e 184 0
e 185 0
e 186 0
e 187 0
e 188 0
e 189 0
e 190 0
e 191 0
e 192 0
e 193 0
e 194 0
e 195 0
e 196 0
e 197 0
e 198 0
e 199 0
e 200 0
e 201 0
e 202 0
e 203 0
e 204 0
e 205 0
e 206 0
e 207 0
e 208 0
e 209 0
e 210 0
e 211 0
e 212 0
e 213 0
e 214 0
e 215 0
e 216 0
e 217 0
e 218 0
e 219 0
e 220 0
e 221 0
e 222 0
e 223 0
e 224 0
e 225 0
e 226 0
e 227 0
e 228 0
e 229 0
e 230 0
e 231 0
e 232 0
e 233 0
e 234 0
e 235 0
e 236 0
e 237 0
e 238 0
e 239 0
e 240 0
e 241 0
e 242 0
e 243 0
e 244 0
e 245 0
e 246 0
e 247 0
e 248 0
e 249 0
e 250 0
e 251 0
e 252 0
e 253 0
e 254 0
e 255 0
e 256 0
e 257 0
e 258 0
e 259 0
e 260 0
e 261 0
e 262 0
e 263 0
e 264 0
e 265 0
e 266 0
e 267 0
e 268 0
e 269 0
e 270 0
e 271 0
e 272 0
e 273 0
e 274 0
e 275 0
e 276 0
e 277 0
e 278 0
e 279 0
e 280 0
e 281 0
e 282 0
e 283 0
e 284 0
e 285 0
e 286 0
e 287 0
e 288 0
e 289 0
e 290 0
e 291 0
e 292 0
e 293 0
e 294 0
e 295 0
e 296 0
e 297 0
e 298 0
e 299 0
e 300 0
e 301 0
e 302 0
e 303 0
e 304 0
e 305 0
e 306 0
e 307 0
e 308 0
e 309 0
e 310 0
e 311 0
e 312 0
e 313 0
e 314 0
e 315 0
e 316 0
e 317 0
e 318 0
e 319 0
e 320 0
e 321 0
e 322 0
e 323 0
e 324 0
e 325 0
e 326 0
e 327 0
e 328 0
e 329 0
e 330 0
e 331 0
e 332 0
e 333 0
e 334 0
e 335 0
e 336 0
e 337 0
e 338 0
e 339 0
e 340 0
e 341 0
e 342 0
e 343 0
e 344 0
e 345 0
e 346 0
e 347 0
e 348 0
e 349 0
e 350 0
e 351 0
e 352 0
e 353 0
e 354 0
e 355 0
e 356 0
e 357 0
e 358 0
e 359 0
e 360 0
e 361 0
e 362 0
e 363 0
e 364 0
e 365 0
e 366 0
e 367 0
e 368 0
e 369 0
e 370 0
e 371 0
e 372 0
e 373 0
e 374 0
e 375 0
e 376 0
e 377 0
e 378 0
e 379 0
e 380 0
e 381 0
e 382 0
e 383 0
e 384 0
e 385 0
e 386 0
e 387 0
e 388 0
e 389 0
e 390 0
e 391 0
e 392 0
e 393 0
e 394 0
e 395 0
e 396 0
e 397 0
e 398 0
e 399 0
e 400 0
e 401 0
e 402 0
e 403 0
e 404 0
e 405 0
e 406 0
e 407 0
e 408 0
e 409 0
e 410 0
e 411 0
e 412 0
e 413 0
e 414 0
e 415 0
e 416 0
e 417 0
e 418 0
e 419 0
e 420 0
e 421 0
e 422 0
e 423 0
e 424 0
e 425 0
e 426 0
e 427 0
e 428 0
e 429 0
e 430 0
e 431 0
e 432 0
e 433 0
e 434 0
e 435 0
e 436 0
e 437 0
e 438 0
e 439 0
e 440 0
e 441 0
e 442 0
e 443 0
e 444 0
e 445 0
e 446 0
e 447 0
e 448 0
e 449 0
e 450 0
e 451 0
e 452 0
e 453 0
e 454 0
e 455 0
e 456 0
e 457 0
e 458 0
e 459 0
e 460 0
e 461 0
e 462 0
e 463 0
e 464 0
e 465 0
e 466 0
e 467 0
e 468 0
e 469 0
e 470 0
e 471 0
e 472 0
e 473 0
e 474 0
e 475 0
e 476 0
e 477 0
e 478 0
e 479 0
e 480 0
e 481 0
e 482 0
e 483 0
e 484 0
e 485 0
e 486 0
e 487 0
e 488 0
e 489 0
e 490 0
e 491 0
e 492 0
e 493 0
e 494 0
e 495 0
e 496 0
e 497 0
e 498 0
e 499 0
e 500 0
e 501 0
e 502 0
e 503 0
e 504 0
e 505 0
e 506 0
e 507 0
e 508 0
e 509 0
e 510 0
e 511 0
e 512 0
e 513 0
e 514 0
e 515 0
e 516 0
e 517 0
e 518 0
e 519 0
e 520 0
e 521 0
e 522 0
e 523 0
e 524 0
e 525 0
e 526 0
e 527 0
e 528 0
e 529 0
e 530 0
e 531 0
e 532 0
e 533 0
e 534 0
e 535 0
e 536 0
e 537 0
e 538 0
e 539 0
e 540 0
e 541 0
e 542 0
e 543 0
e 544 0
e 545 0
e 546 0
e 547 0
e 548 0
e 549 0
e 550 0
e 551 0
e 552 0
e 553 0
e 554 0
e 555 0
e 556 0
e 557 0
e 558 0
e 559 0
e 560 0
e 561 0
e 562 0
e 563 0
e 564 0
e 565 0
e 566 0
e 567 0
e 568 0
e 569 0
e 570 0
e 571 0
e 572 0
e 573 0
e 574 0
e 575 0
e 576 0
e 577 0
e 578 0
e 579 0
e 580 0
e 581 0
e 582 0
e 583 0
e 584 0
e 585 0
e 586 0
e 587 0
e 588 0
e 589 0
e 590 0
e 591 0
e 592 0
e 593 0
e 594 0
e 595 0
e 596 0
e 597 0
e 598 0
e 599 0
e 600 0
e 601 0
e 602 0
e 603 0
e 604 0
e 605 0
e 606 0
e 607 0
e 608 0
e 609 0
e 610 0
e 611 0
e 612 0
e 613 0
e 614 0
e 615 0
e 616 0
e 617 0
e 618 0
e 619 0
e 620 0
e 621 0
e 622 0
e 623 0
e 624 0
e 625 0
e 626 0
e 627 0
e 628 0
e 629 0
e 630 0
e 631 0
e 632 0
e 633 0
e 634 0
e 635 0
e 636 0
e 637 0
e 638 0
e 639 0
e 640 0
e 641 0
e 642 0
e 643 0
e 644 0
e 645 0
e 646 0
e 647 0
e 648 0
e 649 0
e 650 0
e 651 0
e 652 0
e 653 0
e 654 0
e 655 0
e 656 0
e 657 0
e 658 0
e 659 0
e 660 0
e 661 0
e 662 0
e 663 0
e 664 0
e 665 0
e 666 0
e 667 0
e 668 0
e 669 0
e 670 0
e 671 0
e 672 0
e 673 0
e 674 0
e 675 0
e 676 0
e 677 0
e 678 0
e 679 0
e 680 0
e 681 0
e 682 0
e 683 0
e 684 0
e 685 0
e 686 0
e 687 0
e 688 0
e 689 0
e 690 0
e 691 0
e 692 0
e 693 0
24 18 0
-24 -18 0
25 18 0
-25 -18 0
26 18 0
-26 -18 0
27 18 0
-27 -18 0
28 18 0
-28 -18 0
29 9 0
-29 -9 0
30 6 0
-30 -6 0
31 13 0
-31 -13 0
32 11 0
-32 -11 0
33 12 0
-33 -12 0
34 3 0
-34 -3 0
35 10 0
-35 -10 0
36 14 0
-36 -14 0
37 8 0
-37 -8 0
38 7 0
-38 -7 0
39 1 0
-39 -1 0
40 5 0
-40 -5 0
41 16 0
-41 -16 0
42 19 0
-42 -19 0
43 17 0
-43 -17 0
44 22 0
-44 -22 0
45 21 0
-45 -21 0
46 20 0
-46 -20 0
47 2 0
-47 -2 0
48 23 0
-48 -23 0
-49 19 0
-49 44 0
49 -19 -44 0
-311 44 0
-311 20 0
311 -44 -20 0
-312 311 0
-312 42 0
312 -311 -42 0
-50 312 0
-50 2 0
50 -312 -2 0
-313 20 0
-313 19 0
313 -20 -19 0
-51 313 0
-51 39 0
51 -313 -39 0
-314 23 0
-314 21 0
314 -23 -21 0
-52 314 0
-52 20 0
52 -314 -20 0
-315 48 0
-315 45 0
315 -48 -45 0
-53 315 0
-53 46 0
53 -315 -46 0
-316 48 0
-316 44 0
316 -48 -44 0
-317 316 0
-317 20 0
317 -316 -20 0
-54 317 0
-54 19 0
54 -317 -19 0
-318 21 0
-318 46 0
318 -21 -46 0
-55 318 0
-55 42 0
55 -318 -42 0
-56 45 0
-56 20 0
56 -45 -20 0
-57 43 0
-57 21 0
57 -43 -21 0
-58 5 0
-58 21 0
58 -5 -21 0
-319 48 0
-319 44 0
319 -48 -44 0
-59 319 0
-59 6 0
59 -319 -6 0
-60 23 0
-60 4 0
60 -23 -4 0
-61 23 0
-61 2 0
61 -23 -2 0
-62 23 0
-62 22 0
62 -23 -22 0
-63 44 0
-63 23 0
63 -44 -23 0
-320 23 0
-320 22 0
320 -23 -22 0
-321 320 0
-321 19 0
321 -320 -19 0
-64 321 0
-64 39 0
64 -321 -39 0
-322 44 0
-322 19 0
322 -44 -19 0
-65 322 0
-65 40 0
65 -322 -40 0
-66 31 0
-66 33 0
66 -31 -33 0
-67 33 0
-67 32 0
67 -33 -32 0
-323 48 0
-323 44 0
323 -48 -44 0
-68 323 0
-68 6 0
68 -323 -6 0
-69 23 0
-69 4 0
69 -23 -4 0
-70 23 0
-70 2 0
70 -23 -2 0
-71 23 0
-71 22 0
71 -23 -22 0
-72 44 0
-72 23 0
72 -44 -23 0
-73 48 0
-73 12 0
73 -48 -12 0
-74 48 0
-74 11 0
74 -48 -11 0
-75 23 0
-75 22 0
75 -23 -22 0
-324 23 0
-324 22 0
324 -23 -22 0
-325 324 0
-325 19 0
325 -324 -19 0
-76 325 0
-76 39 0
76 -325 -39 0
-326 44 0
-326 19 0
326 -44 -19 0
-77 326 0
-77 40 0
77 -326 -40 0
-327 48 0
-327 44 0
327 -48 -44 0
-78 327 0
-78 17 0
78 -327 -17 0
-328 44 0
-328 17 0
328 -44 -17 0
-79 328 0
-79 41 0
79 -328 -41 0
-80 23 0
-80 22 0
80 -23 -22 0
-329 48 0
-329 19 0
329 -48 -19 0
-81 329 0
-81 16 0
81 -329 -16 0
-82 44 0
-82 41 0
82 -44 -41 0
-83 46 0
-83 19 0
83 -46 -19 0
-84 46 0
-84 16 0
84 -46 -16 0
-330 23 0
-330 44 0
330 -23 -44 0
-331 330 0
-331 21 0
331 -330 -21 0
-85 331 0
-85 16 0
85 -331 -16 0
-86 48 0
-86 45 0
86 -48 -45 0
-332 48 0
-332 22 0
332 -48 -22 0
-87 332 0
-87 21 0
87 -332 -21 0
-333 23 0
-333 21 0
333 -23 -21 0
-88 333 0
-88 20 0
88 -333 -20 0
-89 44 0
-89 46 0
89 -44 -46 0
-90 45 0
-90 46 0
90 -45 -46 0
-91 41 0
-91 45 0
91 -41 -45 0
-92 41 0
-92 48 0
92 -41 -48 0
-334 48 0
-334 19 0
334 -48 -19 0
-93 334 0
-93 1 0
93 -334 -1 0
-335 42 0
-335 43 0
335 -42 -43 0
-94 335 0
-94 47 0
94 -335 -47 0
-95 23 0
-95 42 0
95 -23 -42 0
-96 23 0
-96 43 0
96 -23 -43 0
-97 48 0
-97 45 0
97 -48 -45 0
-98 44 0
-98 45 0
98 -44 -45 0
336 -2 0
336 -21 0
-336 2 21 0
99 -336 0
99 -22 0
-99 336 22 0
100 -16 0
100 -48 0
-100 16 48 0
337 -48 0
337 -41 0
-337 48 41 0
101 -337 0
101 -36 0
-101 337 36 0
102 -23 0
102 -42 0
-102 23 42 0
103 -23 0
103 -16 0
-103 23 16 0
338 -35 0
338 -29 0
-338 35 29 0
339 -338 0
339 -37 0
-339 338 37 0
104 -339 0
104 -38 0
-104 339 38 0
340 -48 0
340 -46 0
-340 48 46 0
105 -340 0
105 -41 0
-105 340 41 0
106 -23 0
106 -20 0
-106 23 20 0
107 -44 0
107 -20 0
-107 44 20 0
108 -13 0
108 -12 0
-108 13 12 0
109 -13 0
109 -11 0
-109 13 11 0
110 -12 0
110 -11 0
-110 12 11 0
341 -23 0
341 -13 0
-341 23 13 0
342 -341 0
342 -12 0
-342 341 12 0
111 -342 0
111 -32 0
-111 342 32 0
343 -23 0
343 -13 0
-343 23 13 0
344 -343 0
344 -33 0
-344 343 33 0
112 -344 0
112 -11 0
-112 344 11 0
113 -23 0
113 -42 0
-113 23 42 0
114 -21 0
114 -42 0
-114 21 42 0
115 -43 0
115 -5 0
-115 43 5 0
116 -23 0
116 -17 0
-116 23 17 0
117 -22 0
117 -17 0
-117 22 17 0
345 -20 0
345 -19 0
-345 20 19 0
346 -345 0
346 -41 0
-346 345 41 0
118 -346 0
118 -15 0
-118 346 15 0
347 -22 0
347 -20 0
-347 22 20 0
119 -347 0
119 -19 0
-119 347 19 0
120 -22 0
120 -23 0
-120 22 23 0
121 -44 0
121 -19 0
-121 44 19 0
122 -44 0
122 -16 0
-122 44 16 0
348 -48 0
348 -45 0
-348 48 45 0
123 -348 0
123 -46 0
-123 348 46 0
349 -21 0
349 -20 0
-349 21 20 0
124 -349 0
124 -17 0
-124 349 17 0
350 -23 0
350 -21 0
-350 23 21 0
351 -350 0
351 -41 0
-351 350 41 0
125 -351 0
125 -15 0
-125 351 15 0
352 -23 0
352 -22 0
-352 23 22 0
126 -352 0
126 -21 0
-126 352 21 0
353 -48 0
353 -44 0
-353 48 44 0
127 -353 0
127 -40 0
-127 353 40 0
128 -45 0
128 -40 0
-128 45 40 0
129 -48 0
129 -22 0
-129 48 22 0
130 -22 0
130 -6 0
-130 22 6 0
131 -48 0
131 -43 0
-131 48 43 0
132 -20 0
132 -5 0
-132 20 5 0
133 -46 0
133 -19 0
-133 46 19 0
134 -46 0
134 -39 0
-134 46 39 0
135 -44 0
135 -23 0
-135 44 23 0
136 -6 0
136 -23 0
-136 6 23 0
-355 16 0
-355 42 0
355 -16 -42 0
-356 355 0
-356 46 0
356 -355 -46 0
-354 356 0
-354 45 0
354 -356 -45 0
137 354 0
-137 -354 0
-358 30 0
-358 42 0
358 -30 -42 0
-359 358 0
-359 20 0
359 -358 -20 0
-357 359 0
-357 21 0
357 -359 -21 0
138 357 0
-138 -357 0
-361 42 0
-361 46 0
361 -42 -46 0
-362 361 0
-362 45 0
362 -361 -45 0
-360 362 0
-360 22 0
360 -362 -22 0
139 360 0
-139 -360 0
-364 6 0
-364 42 0
364 -6 -42 0
-365 364 0
-365 20 0
365 -364 -20 0
-363 365 0
-363 21 0
363 -365 -21 0
140 363 0
-140 -363 0
-367 17 0
-367 46 0
367 -17 -46 0
-368 367 0
-368 21 0
368 -367 -21 0
-366 368 0
-366 22 0
366 -368 -22 0
141 366 0
-141 -366 0
-370 113 0
-370 112 0
370 -113 -112 0
-369 370 0
-369 111 0
369 -370 -111 0
142 369 0
-142 -369 0
143 117 0
143 116 0
-143 -117 -116 0
-372 45 0
-372 22 0
372 -45 -22 0
-371 372 0
-371 23 0
371 -372 -23 0
144 371 0
-144 -371 0
-374 21 0
-374 22 0
374 -21 -22 0
-373 374 0
-373 23 0
373 -374 -23 0
145 373 0
-145 -373 0
-376 134 0
-376 133 0
376 -134 -133 0
-375 376 0
-375 132 0
375 -376 -132 0
146 375 0
-146 -375 0
-378 10 0
-378 16 0
378 -10 -16 0
-379 378 0
-379 21 0
379 -378 -21 0
-377 379 0
-377 48 0
377 -379 -48 0
147 377 0
-147 -377 0
-381 40 0
-381 110 0
381 -40 -110 0
-382 381 0
-382 109 0
382 -381 -109 0
-380 382 0
-380 108 0
380 -382 -108 0
148 380 0
-148 -380 0
-384 43 0
-384 42 0
384 -43 -42 0
-383 384 0
-383 46 0
383 -384 -46 0
149 383 0
-149 -383 0
-386 16 0
-386 42 0
386 -16 -42 0
-387 386 0
-387 22 0
387 -386 -22 0
-385 387 0
-385 23 0
385 -387 -23 0
150 385 0
-150 -385 0
151 119 0
151 118 0
-151 -119 -118 0
152 9 0
152 10 0
-152 -9 -10 0
153 122 0
153 121 0
-153 -122 -121 0
154 124 0
154 123 0
-154 -124 -123 0
-389 128 0
-389 127 0
389 -128 -127 0
-390 389 0
-390 126 0
390 -389 -126 0
-388 390 0
-388 125 0
388 -390 -125 0
155 388 0
-155 -388 0
-392 40 0
-392 22 0
392 -40 -22 0
-391 392 0
-391 48 0
391 -392 -48 0
156 391 0
-156 -391 0
-394 21 0
-394 131 0
394 -21 -131 0
-395 394 0
-395 130 0
395 -394 -130 0
-393 395 0
-393 129 0
393 -395 -129 0
157 393 0
-157 -393 0
158 45 0
158 104 0
-158 -45 -104 0
-397 21 0
-397 103 0
397 -21 -103 0
-398 397 0
-398 102 0
398 -397 -102 0
-396 398 0
-396 101 0
396 -398 -101 0
159 396 0
-159 -396 0
-400 45 0
-400 107 0
400 -45 -107 0
-401 400 0
-401 106 0
401 -400 -106 0
-399 401 0
-399 105 0
399 -401 -105 0
160 399 0
-160 -399 0
161 44 0
161 23 0
-161 -44 -23 0
-403 42 0
-403 20 0
403 -42 -20 0
-404 403 0
-404 21 0
404 -403 -21 0
-402 404 0
-402 44 0
402 -404 -44 0
162 402 0
-162 -402 0
-406 16 0
-406 20 0
406 -16 -20 0
-407 406 0
-407 45 0
407 -406 -45 0
-405 407 0
-405 44 0
405 -407 -44 0
163 405 0
-163 -405 0
-409 40 0
-409 20 0
409 -40 -20 0
-410 409 0
-410 45 0
410 -409 -45 0
-408 410 0
-408 22 0
408 -410 -22 0
164 408 0
-164 -408 0
-412 42 0
-412 20 0
412 -42 -20 0
-413 412 0
-413 21 0
413 -412 -21 0
-411 413 0
-411 22 0
411 -413 -22 0
165 411 0
-165 -411 0
-415 15 0
-415 16 0
415 -15 -16 0
-416 415 0
-416 42 0
416 -415 -42 0
-414 416 0
-414 46 0
414 -416 -46 0
166 414 0
-166 -414 0
167 115 0
167 114 0
-167 -115 -114 0
-418 42 0
-418 20 0
418 -42 -20 0
-419 418 0
-419 21 0
419 -418 -21 0
-417 419 0
-417 44 0
417 -419 -44 0
168 417 0
-168 -417 0
-421 17 0
-421 42 0
421 -17 -42 0
-422 421 0
-422 20 0
422 -421 -20 0
-420 422 0
-420 21 0
420 -422 -21 0
169 420 0
-169 -420 0
170 44 0
170 48 0
-170 -44 -48 0
171 22 0
171 23 0
-171 -22 -23 0
-424 42 0
-424 20 0
424 -42 -20 0
-425 424 0
-425 21 0
425 -424 -21 0
-423 425 0
-423 44 0
423 -425 -44 0
172 423 0
-172 -423 0
-427 16 0
-427 20 0
427 -16 -20 0
-428 427 0
-428 45 0
428 -427 -45 0
-426 428 0
-426 44 0
426 -428 -44 0
173 426 0
-173 -426 0
430 -137 0
430 -44 0
-430 137 44 0
429 -430 0
429 -23 0
-429 430 23 0
174 429 0
-174 -429 0
432 -138 0
432 -22 0
-432 138 22 0
431 -432 0
431 -23 0
-431 432 23 0
175 431 0
-175 -431 0
-176 -42 0
-176 -21 0
176 42 21 0
434 -56 0
434 -55 0
-434 56 55 0
433 -434 0
433 -54 0
-433 434 54 0
177 433 0
-177 -433 0
-178 -139 0
-178 -23 0
178 139 23 0
436 -140 0
436 -22 0
-436 140 22 0
435 -436 0
435 -23 0
-435 436 23 0
179 435 0
-179 -435 0
438 -36 0
438 -41 0
-438 36 41 0
437 -438 0
437 -43 0
-437 438 43 0
180 437 0
-180 -437 0
-181 -51 0
-181 -50 0
181 51 50 0
-182 -19 0
-182 -20 0
182 19 20 0
-183 -148 0
-183 -41 0
183 148 41 0
440 -35 0
440 -41 0
-440 35 41 0
439 -440 0
439 -42 0
-439 440 42 0
184 439 0
-184 -439 0
442 -42 0
442 -22 0
-442 42 22 0
441 -442 0
441 -23 0
-441 442 23 0
185 441 0
-185 -441 0
-186 -40 0
-186 -46 0
186 40 46 0
-187 -22 0
-187 -23 0
187 22 23 0
444 -149 0
444 -2 0
-444 149 2 0
445 -444 0
445 -34 0
-445 444 34 0
443 -445 0
443 -4 0
-443 445 4 0
188 443 0
-188 -443 0
447 -41 0
447 -43 0
-447 41 43 0
446 -447 0
446 -19 0
-446 447 19 0
189 446 0
-189 -446 0
449 -20 0
449 -45 0
-449 20 45 0
450 -449 0
450 -44 0
-450 449 44 0
448 -450 0
448 -23 0
-448 450 23 0
190 448 0
-190 -448 0
-191 -67 0
-191 -66 0
191 67 66 0
452 -90 0
452 -89 0
-452 90 89 0
453 -452 0
453 -88 0
-453 452 88 0
451 -453 0
451 -87 0
-451 453 87 0
192 451 0
-192 -451 0
455 -96 0
455 -95 0
-455 96 95 0
456 -455 0
456 -94 0
-456 455 94 0
454 -456 0
454 -93 0
-454 456 93 0
193 454 0
-193 -454 0
458 -181 0
458 -45 0
-458 181 45 0
459 -458 0
459 -48 0
-459 458 48 0
457 -459 0
457 -49 0
-457 459 49 0
194 457 0
-194 -457 0
461 -62 0
461 -61 0
-461 62 61 0
462 -461 0
462 -60 0
-462 461 60 0
460 -462 0
460 -59 0
-460 462 59 0
195 460 0
-195 -460 0
-196 -65 0
-196 -64 0
196 65 64 0
-197 -74 0
-197 -73 0
197 74 73 0
-198 -42 0
-198 -75 0
198 42 75 0
464 -2 0
464 -34 0
-464 2 34 0
465 -464 0
465 -4 0
-465 464 4 0
463 -465 0
463 -17 0
-463 465 17 0
199 463 0
-199 -463 0
467 -71 0
467 -70 0
-467 71 70 0
468 -467 0
468 -69 0
-468 467 69 0
466 -468 0
466 -68 0
-466 468 68 0
200 466 0
-200 -466 0
-201 -77 0
-201 -76 0
201 77 76 0
470 -35 0
470 -41 0
-470 35 41 0
469 -470 0
469 -42 0
-469 470 42 0
202 469 0
-202 -469 0
472 -84 0
472 -83 0
-472 84 83 0
473 -472 0
473 -82 0
-473 472 82 0
471 -473 0
471 -81 0
-471 473 81 0
203 471 0
-203 -471 0
475 -45 0
475 -44 0
-475 45 44 0
474 -475 0
474 -48 0
-474 475 48 0
204 474 0
-204 -474 0
477 -80 0
477 -79 0
-477 80 79 0
476 -477 0
476 -78 0
-476 477 78 0
205 476 0
-205 -476 0
-206 -4 0
-206 -22 0
206 4 22 0
-207 -86 0
-207 -85 0
207 86 85 0
479 -42 0
479 -22 0
-479 42 22 0
478 -479 0
478 -23 0
-478 479 23 0
208 478 0
-208 -478 0
-209 -40 0
-209 -46 0
209 40 46 0
-210 -160 0
-210 -92 0
210 160 92 0
481 -21 0
481 -44 0
-481 21 44 0
480 -481 0
480 -23 0
-480 481 23 0
211 480 0
-211 -480 0
-212 -98 0
-212 -97 0
212 98 97 0
-213 -162 0
-213 -23 0
213 162 23 0
-214 -163 0
-214 -23 0
214 163 23 0
-215 -165 0
-215 -23 0
215 165 23 0
483 -166 0
483 -21 0
-483 166 21 0
484 -483 0
484 -44 0
-484 483 44 0
482 -484 0
482 -23 0
-482 484 23 0
216 482 0
-216 -482 0
-217 -44 0
-217 -48 0
217 44 48 0
-218 -168 0
-218 -48 0
218 168 48 0
486 -169 0
486 -44 0
-486 169 44 0
485 -486 0
485 -48 0
-485 486 48 0
219 485 0
-219 -485 0
-220 -53 0
-220 -52 0
220 53 52 0
-221 -172 0
-221 -48 0
221 172 48 0
-222 -173 0
-222 -48 0
222 173 48 0
-223 159 0
-223 46 0
223 -159 -46 0
-487 193 0
-487 46 0
487 -193 -46 0
-488 487 0
-488 45 0
488 -487 -45 0
-224 488 0
-224 44 0
224 -488 -44 0
225 -185 0
225 -45 0
-225 185 45 0
-489 204 0
-489 39 0
489 -204 -39 0
-490 489 0
-490 19 0
490 -489 -19 0
-226 490 0
-226 20 0
226 -490 -20 0
-491 211 0
-491 15 0
491 -211 -15 0
-492 491 0
-492 16 0
492 -491 -16 0
-227 492 0
-227 46 0
227 -492 -46 0
228 -199 0
228 -22 0
-228 199 22 0
-494 184 0
-494 7 0
494 -184 -7 0
-495 494 0
-495 8 0
495 -494 -8 0
-493 495 0
-493 9 0
493 -495 -9 0
229 493 0
-229 -493 0
-496 212 0
-496 5 0
496 -212 -5 0
-230 496 0
-230 46 0
230 -496 -46 0
497 -153 0
497 -152 0
-497 153 152 0
498 -497 0
498 -38 0
-498 497 38 0
231 -498 0
231 -37 0
-231 498 37 0
-500 182 0
-500 47 0
500 -182 -47 0
-501 500 0
-501 4 0
501 -500 -4 0
-499 501 0
-499 43 0
499 -501 -43 0
232 499 0
-232 -499 0
-502 205 0
-502 40 0
502 -205 -40 0
-503 502 0
-503 20 0
503 -502 -20 0
-233 503 0
-233 45 0
233 -503 -45 0
234 186 0
234 225 0
-234 -186 -225 0
-504 197 0
-504 16 0
504 -197 -16 0
-505 504 0
-505 21 0
505 -504 -21 0
-235 505 0
-235 22 0
235 -505 -22 0
-236 150 0
-236 45 0
236 -150 -45 0
-237 200 0
-237 42 0
237 -200 -42 0
-506 154 0
-506 206 0
506 -154 -206 0
-507 506 0
-507 47 0
507 -506 -47 0
-238 507 0
-238 3 0
238 -507 -3 0
-239 229 0
-239 17 0
239 -229 -17 0
508 -176 0
508 -20 0
-508 176 20 0
509 -508 0
509 -44 0
-509 508 44 0
240 -509 0
240 -48 0
-240 509 48 0
510 -142 0
510 -141 0
-510 142 141 0
511 -510 0
511 -5 0
-511 510 5 0
241 -511 0
241 -41 0
-241 511 41 0
512 -143 0
512 -5 0
-512 143 5 0
513 -512 0
513 -46 0
-513 512 46 0
242 -513 0
242 -21 0
-242 513 21 0
514 -198 0
514 -236 0
-514 198 236 0
243 -514 0
243 -235 0
-243 514 235 0
515 -243 0
515 -5 0
-515 243 5 0
516 -515 0
516 -43 0
-516 515 43 0
244 -516 0
244 -20 0
-244 516 20 0
-245 -233 0
-245 -226 0
245 233 226 0
246 -208 0
246 -45 0
-246 208 45 0
517 -161 0
517 -2 0
-517 161 2 0
518 -517 0
518 -3 0
-518 517 3 0
247 -518 0
247 -4 0
-247 518 4 0
519 -180 0
519 -145 0
-519 180 145 0
520 -519 0
520 -5 0
-520 519 5 0
248 -520 0
248 -20 0
-248 520 20 0
521 -167 0
521 -20 0
-521 167 20 0
522 -521 0
522 -44 0
-522 521 44 0
249 -522 0
249 -48 0
-249 522 48 0
523 -217 0
523 -17 0
-523 217 17 0
524 -523 0
524 -46 0
-524 523 46 0
250 -524 0
250 -21 0
-250 524 21 0
525 -170 0
525 -19 0
-525 170 19 0
526 -525 0
526 -20 0
-526 525 20 0
251 -526 0
251 -21 0
-251 526 21 0
527 -171 0
527 -19 0
-527 171 19 0
528 -527 0
528 -46 0
-528 527 46 0
252 -528 0
252 -45 0
-252 528 45 0
-530 183 0
-530 17 0
530 -183 -17 0
-531 530 0
-531 42 0
531 -530 -42 0
-529 531 0
-529 46 0
529 -531 -46 0
253 529 0
-253 -529 0
532 -146 0
532 -45 0
-532 146 45 0
533 -532 0
533 -44 0
-533 532 44 0
254 -533 0
254 -48 0
-254 533 48 0
255 177 0
255 240 0
-255 -177 -240 0
-256 -196 0
-256 -63 0
256 196 63 0
534 -147 0
534 -38 0
-534 147 38 0
535 -534 0
535 -8 0
-535 534 8 0
257 -535 0
257 -9 0
-257 535 9 0
-258 207 0
-258 17 0
258 -207 -17 0
-537 188 0
-537 45 0
537 -188 -45 0
-538 537 0
-538 44 0
538 -537 -44 0
-536 538 0
-536 48 0
536 -538 -48 0
259 536 0
-259 -536 0
-260 -201 0
-260 -72 0
260 201 72 0
-261 156 0
-261 46 0
261 -156 -46 0
-540 151 0
-540 45 0
540 -151 -45 0
-541 540 0
-541 48 0
541 -540 -48 0
-539 541 0
-539 228 0
539 -541 -228 0
262 539 0
-262 -539 0
-263 195 0
-263 42 0
263 -195 -42 0
-543 203 0
-543 120 0
543 -203 -120 0
-542 543 0
-542 231 0
542 -543 -231 0
264 542 0
-264 -542 0
265 209 0
265 246 0
-265 -209 -246 0
-266 -155 0
-266 -258 0
266 155 258 0
-267 -157 0
-267 -261 0
267 157 261 0
-544 187 0
-544 47 0
544 -187 -47 0
-545 544 0
-545 17 0
545 -544 -17 0
-268 545 0
-268 45 0
268 -545 -45 0
547 -164 0
547 -48 0
-547 164 48 0
546 -547 0
546 -239 0
-546 547 239 0
269 546 0
-269 -546 0
-548 191 0
-548 190 0
548 -191 -190 0
-549 548 0
-549 189 0
549 -548 -189 0
-270 549 0
-270 40 0
270 -549 -40 0
551 -232 0
551 -21 0
-551 232 21 0
552 -551 0
552 -22 0
-552 551 22 0
550 -552 0
550 -23 0
-550 552 23 0
271 550 0
-271 -550 0
-553 202 0
-553 7 0
553 -202 -7 0
-554 553 0
-554 8 0
554 -553 -8 0
-272 554 0
-272 9 0
272 -554 -9 0
556 -58 0
556 -57 0
-556 58 57 0
555 -556 0
555 -268 0
-555 556 268 0
273 555 0
-273 -555 0
-557 192 0
-557 40 0
557 -192 -40 0
-558 557 0
-558 17 0
558 -557 -17 0
-274 558 0
-274 19 0
274 -558 -19 0
560 -220 0
560 -47 0
-560 220 47 0
561 -560 0
561 -19 0
-561 560 19 0
559 -561 0
559 -22 0
-559 561 22 0
275 559 0
-275 -559 0
-562 158 0
-562 19 0
562 -158 -19 0
-276 562 0
-276 20 0
276 -562 -20 0
-564 100 0
-564 99 0
564 -100 -99 0
-563 564 0
-563 257 0
563 -564 -257 0
277 563 0
-277 -563 0
278 252 0
278 251 0
-278 -252 -251 0
566 -253 0
566 -45 0
-566 253 45 0
567 -566 0
567 -44 0
-567 566 44 0
565 -567 0
565 -23 0
-565 567 23 0
279 565 0
-279 -565 0
568 -264 0
568 -5 0
-568 264 5 0
569 -568 0
569 -43 0
-569 568 43 0
280 -569 0
280 -21 0
-280 569 21 0
-281 266 0
-281 46 0
281 -266 -46 0
570 -273 0
570 -19 0
-570 273 19 0
282 -570 0
282 -20 0
-282 570 20 0
572 -91 0
572 -223 0
-572 91 223 0
571 -572 0
571 -276 0
-571 572 276 0
283 571 0
-283 -571 0
-284 -256 0
-284 -263 0
284 256 263 0
-285 -43 0
-285 -272 0
285 43 272 0
-286 -260 0
-286 -237 0
286 260 237 0
-574 136 0
-574 135 0
574 -136 -135 0
-573 574 0
-573 247 0
573 -574 -247 0
287 573 0
-287 -573 0
-575 277 0
-575 42 0
575 -277 -42 0
-288 575 0
-288 46 0
288 -575 -46 0
577 -267 0
577 -281 0
-577 267 281 0
576 -577 0
576 -238 0
-576 577 238 0
289 576 0
-289 -576 0
-290 283 0
-290 22 0
290 -283 -22 0
578 -194 0
578 -224 0
-578 194 224 0
579 -578 0
579 -274 0
-579 578 274 0
291 -579 0
291 -270 0
-291 579 270 0
-580 287 0
-580 20 0
580 -287 -20 0
-292 580 0
-292 21 0
292 -580 -21 0
581 -285 0
581 -144 0
-581 285 144 0
582 -581 0
582 -5 0
-582 581 5 0
293 -582 0
293 -46 0
-293 582 46 0
-584 234 0
-584 282 0
584 -234 -282 0
-585 584 0
-585 250 0
585 -584 -250 0
-583 585 0
-583 249 0
583 -585 -249 0
294 583 0
-294 -583 0
295 -289 0
295 -19 0
-295 289 19 0
587 -210 0
587 -290 0
-587 210 290 0
586 -587 0
586 -288 0
-586 587 288 0
296 586 0
-296 -586 0
-297 24 0
-297 291 0
297 -24 -291 0
588 -284 0
588 -46 0
-588 284 46 0
298 -588 0
298 -45 0
-298 588 45 0
589 -286 0
589 -46 0
-589 286 46 0
299 -589 0
299 -45 0
-299 589 45 0
591 -292 0
591 -230 0
-591 292 230 0
590 -591 0
590 -227 0
-590 591 227 0
300 590 0
-300 -590 0
-593 259 0
-593 298 0
593 -259 -298 0
-594 593 0
-594 242 0
594 -593 -242 0
-592 594 0
-592 241 0
592 -594 -241 0
301 592 0
-301 -592 0
302 -296 0
302 -43 0
-302 296 43 0
-596 262 0
-596 299 0
596 -262 -299 0
-597 596 0
-597 244 0
597 -596 -244 0
-595 597 0
-595 293 0
595 -597 -293 0
303 595 0
-303 -595 0
304 -300 0
304 -19 0
-304 300 19 0
-599 265 0
-599 302 0
599 -265 -302 0
-600 599 0
-600 304 0
600 -599 -304 0
-598 600 0
-598 254 0
598 -600 -254 0
305 598 0
-305 -598 0
-306 28 0
-306 305 0
306 -28 -305 0
-307 25 0
-307 301 0
307 -25 -301 0
-308 26 0
-308 303 0
308 -26 -303 0
-602 245 0
-602 295 0
602 -245 -295 0
-603 602 0
-603 280 0
603 -602 -280 0
-601 603 0
-601 248 0
601 -603 -248 0
309 601 0
-309 -601 0
-310 27 0
-310 309 0
310 -27 -309 0
-604 222 271 0
-604 -222 -271 0
604 -222 271 0
604 222 -271 0
-605 604 213 0
-605 -604 -213 0
605 -604 213 0
605 604 -213 0
-606 605 178 0
-606 -605 -178 0
606 -605 178 0
606 605 -178 0
-607 606 279 0
-607 -606 -279 0
607 -606 279 0
607 606 -279 0
-608 607 294 0
-608 -607 -294 0
608 -607 294 0
608 607 -294 0
-609 608 297 0
-609 -608 -297 0
609 -608 297 0
609 608 -297 0
609 0
-610 222 271 0
-610 -222 -271 0
610 -222 271 0
610 222 -271 0
-611 610 213 0
-611 -610 -213 0
611 -610 213 0
611 610 -213 0
-612 611 178 0
-612 -611 -178 0
612 -611 178 0
612 611 -178 0
-613 612 279 0
-613 -612 -279 0
613 -612 279 0
613 612 -279 0
-614 613 294 0
-614 -613 -294 0
614 -613 294 0
614 613 -294 0
-615 614 297 0
-615 -614 -297 0
615 -614 297 0
615 614 -297 0
615 0
-616 222 271 0
-616 -222 -271 0
616 -222 271 0
616 222 -271 0
-617 616 213 0
-617 -616 -213 0
617 -616 213 0
617 616 -213 0
-618 617 178 0
-618 -617 -178 0
618 -617 178 0
618 617 -178 0
-619 618 279 0
-619 -618 -279 0
619 -618 279 0
619 618 -279 0
-620 619 294 0
-620 -619 -294 0
620 -619 294 0
620 619 -294 0
-621 620 297 0
-621 -620 -297 0
621 -620 297 0
621 620 -297 0
621 0
-622 222 271 0
-622 -222 -271 0
622 -222 271 0
622 222 -271 0
-623 622 213 0
-623 -622 -213 0
623 -622 213 0
623 622 -213 0
-624 623 178 0
-624 -623 -178 0
624 -623 178 0
624 623 -178 0
-625 624 279 0
-625 -624 -279 0
625 -624 279 0
625 624 -279 0
-626 625 294 0
-626 -625 -294 0
626 -625 294 0
626 625 -294 0
-627 626 297 0
-627 -626 -297 0
627 -626 297 0
627 626 -297 0
627 0
-628 222 271 0
-628 -222 -271 0
628 -222 271 0
628 222 -271 0
-629 628 213 0
-629 -628 -213 0
629 -628 213 0
629 628 -213 0
-630 629 178 0
-630 -629 -178 0
630 -629 178 0
630 629 -178 0
-631 630 279 0
-631 -630 -279 0
631 -630 279 0
631 630 -279 0
-632 631 294 0
-632 -631 -294 0
632 -631 294 0
632 631 -294 0
-633 632 297 0
-633 -632 -297 0
633 -632 297 0
633 632 -297 0
633 0
-634 222 271 0
-634 -222 -271 0
634 -222 271 0
634 222 -271 0
-635 634 213 0
-635 -634 -213 0
635 -634 213 0
635 634 -213 0
-636 635 178 0
-636 -635 -178 0
636 -635 178 0
636 635 -178 0
-637 636 279 0
-637 -636 -279 0
637 -636 279 0
637 636 -279 0
-638 637 294 0
-638 -637 -294 0
638 -637 294 0
638 637 -294 0
-639 638 297 0
-639 -638 -297 0
639 -638 297 0
639 638 -297 0
639 0
-640 222 271 0
-640 -222 -271 0
640 -222 271 0
640 222 -271 0
-641 640 213 0
-641 -640 -213 0
641 -640 213 0
641 640 -213 0
-642 641 178 0
-642 -641 -178 0
642 -641 178 0
642 641 -178 0
-643 642 279 0
-643 -642 -279 0
643 -642 279 0
643 642 -279 0
-644 643 294 0
-644 -643 -294 0
644 -643 294 0
644 643 -294 0
-645 644 297 0
-645 -644 -297 0
645 -644 297 0
645 644 -297 0
645 0
-646 222 271 0
-646 -222 -271 0
646 -222 271 0
646 222 -271 0
-647 646 213 0
-647 -646 -213 0
647 -646 213 0
647 646 -213 0
-648 647 178 0
-648 -647 -178 0
648 -647 178 0
648 647 -178 0
-649 648 279 0
-649 -648 -279 0
649 -648 279 0
649 648 -279 0
-650 649 294 0
-650 -649 -294 0
650 -649 294 0
650 649 -294 0
-651 650 297 0
-651 -650 -297 0
651 -650 297 0
651 650 -297 0
651 0
-652 222 271 0
-652 -222 -271 0
652 -222 271 0
652 222 -271 0
-653 652 213 0
-653 -652 -213 0
653 -652 213 0
653 652 -213 0
-654 653 178 0
-654 -653 -178 0
654 -653 178 0
654 653 -178 0
-655 654 279 0
-655 -654 -279 0
655 -654 279 0
655 654 -279 0
-656 655 294 0
-656 -655 -294 0
656 -655 294 0
656 655 -294 0
-657 656 297 0
-657 -656 -297 0
657 -656 297 0
657 656 -297 0
657 0
-658 222 271 0
-658 -222 -271 0
658 -222 271 0
658 222 -271 0
-659 658 213 0
-659 -658 -213 0
659 -658 213 0
659 658 -213 0
-660 659 178 0
-660 -659 -178 0
660 -659 178 0
660 659 -178 0
-661 660 279 0
-661 -660 -279 0
661 -660 279 0
661 660 -279 0
-662 661 294 0
-662 -661 -294 0
662 -661 294 0
662 661 -294 0
-663 662 297 0
-663 -662 -297 0
663 -662 297 0
663 662 -297 0
663 0
-664 222 271 0
-664 -222 -271 0
664 -222 271 0
664 222 -271 0
-665 664 213 0
-665 -664 -213 0
665 -664 213 0
665 664 -213 0
-666 665 178 0
-666 -665 -178 0
666 -665 178 0
666 665 -178 0
-667 666 279 0
-667 -666 -279 0
667 -666 279 0
667 666 -279 0
-668 667 294 0
-668 -667 -294 0
668 -667 294 0
668 667 -294 0
-669 668 297 0
-669 -668 -297 0
669 -668 297 0
669 668 -297 0
669 0
-670 222 271 0
-670 -222 -271 0
670 -222 271 0
670 222 -271 0
-671 670 213 0
-671 -670 -213 0
671 -670 213 0
671 670 -213 0
-672 671 178 0
-672 -671 -178 0
672 -671 178 0
672 671 -178 0
-673 672 279 0
-673 -672 -279 0
673 -672 279 0
673 672 -279 0
-674 673 294 0
-674 -673 -294 0
674 -673 294 0
674 673 -294 0
-675 674 297 0
-675 -674 -297 0
675 -674 297 0
675 674 -297 0
675 0
-676 222 271 0
-676 -222 -271 0
676 -222 271 0
676 222 -271 0
-677 676 213 0
-677 -676 -213 0
677 -676 213 0
677 676 -213 0
-678 677 178 0
-678 -677 -178 0
678 -677 178 0
678 677 -178 0
-679 678 279 0
-679 -678 -279 0
679 -678 279 0
679 678 -279 0
-680 679 294 0
-680 -679 -294 0
680 -679 294 0
680 679 -294 0
-681 680 297 0
-681 -680 -297 0
681 -680 297 0
681 680 -297 0
681 0
-682 222 271 0
-682 -222 -271 0
682 -222 271 0
682 222 -271 0
-683 682 213 0
-683 -682 -213 0
683 -682 213 0
683 682 -213 0
-684 683 178 0
-684 -683 -178 0
684 -683 178 0
684 683 -178 0
-685 684 279 0
-685 -684 -279 0
685 -684 279 0
685 684 -279 0
-686 685 294 0
-686 -685 -294 0
686 -685 294 0
686 685 -294 0
-687 686 297 0
-687 -686 -297 0
687 -686 297 0
687 686 -297 0
687 0
-688 222 271 0
-688 -222 -271 0
688 -222 271 0
688 222 -271 0
-689 688 213 0
-689 -688 -213 0
689 -688 213 0
689 688 -213 0
-690 689 178 0
-690 -689 -178 0
690 -689 178 0
690 689 -178 0
-691 690 279 0
-691 -690 -279 0
691 -690 279 0
691 690 -279 0
-692 691 294 0
-692 -691 -294 0
692 -691 294 0
692 691 -294 0
-693 692 297 0
-693 -692 -297 0
693 -692 297 0
693 692 -297 0
693 0

@nianzelee Could you help? Thanks!

[nianzelee]

@vuphan314 I took a look of the bug, and found that the bug is caused by wrong parsing of floating numbers. The current parser only reads a floating number up to the sixth digit after the decimal point. It wrongly parsed the probabilities in test case s832a_15_7.sdimacs to zeros, and hence caused the bug.

If you are urgent, a quick workaround is to truncate the probabilities in the test case. I will open another issue to improve the parsing for floating numbers.

[nianzelee]

I have opened the issue #5 to improve the parsing of floating numbers. @vuphan314 , if you agree, I will close this issue.

[vuphan314]

@nianzelee Yes, please mention the floating-point parsing precision in the README and close this issue. Thanks!

[nianzelee]

README updated.