Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32d2.opb |
MD5SUM | a483fc3761bb4050329265bf3a3a7ca5 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 372 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 808 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 808 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 808 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.04284 |
Number of variables | 808 |
Total number of constraints | 5557 |
Number of constraints which are clauses | 5557 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 32 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-04-13 20:04:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3540 boxname=wulflinc8 idbench=156 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a483fc3761bb4050329265bf3a3a7ca5 /oldhome/oroussel/tmp/wulflinc8/normalized-ii32d2.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-ii32d2.opb /oldhome/oroussel/tmp/wulflinc8/normalized-ii32d2.opb IDLAUNCH: 3540 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 913944 kB Buffers: 36528 kB Cached: 64860 kB SwapCached: 0 kB Active: 72392 kB Inactive: 31872 kB HighTotal: 131008 kB HighFree: 62300 kB LowTotal: 903652 kB LowFree: 851644 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6932 kB Slab: 10832 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 20:24:48 (client local time) WITH STATUS 10 IN 1200.19 SECONDS stats: 3540 7 1200.19 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 5557 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 5557 18748 | 1852 0 0 nan | 0.000 % | c | 100 | 5557 18748 | 2037 100 8211 82.1 | 0.006 % | c | 252 | 5557 18748 | 2240 252 19966 79.2 | 0.000 % | c | 477 | 5557 18748 | 2465 477 34035 71.4 | 0.000 % | c | 816 | 5557 18748 | 2711 816 61162 75.0 | 0.000 % | c | 1322 | 5557 18748 | 2982 1322 101974 77.1 | 0.000 % | c | 2082 | 5557 18748 | 3280 2082 175391 84.2 | 0.000 % | c | 3222 | 5557 18748 | 3609 3222 287281 89.2 | 0.000 % | c | 4930 | 5557 18748 | 3969 3034 259982 85.7 | 0.000 % | c | 7492 | 5557 18748 | 4366 3524 289629 82.2 | 0.000 % | c ============================================================================== c [1mFound solution: 386[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 1608 maxlim: 422 bits: 10/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8400 | 16764 58762 | 5588 4432 356590 80.5 | 0.000 % | c | 8500 | 16764 58762 | 6146 4532 364609 80.5 | 0.248 % | c | 8650 | 16764 58762 | 6761 4682 375257 80.1 | 0.248 % | c | 8880 | 16764 58762 | 7437 4912 395122 80.4 | 0.248 % | c | 9217 | 16764 58762 | 8181 5249 424325 80.8 | 0.248 % | c | 9723 | 16764 58762 | 8999 5755 458152 79.6 | 0.248 % | c | 10482 | 16764 58762 | 9899 6514 522630 80.2 | 0.248 % | c | 11621 | 16764 58762 | 10889 7653 604776 79.0 | 0.248 % | c | 13331 | 16764 58762 | 11978 9363 736158 78.6 | 0.248 % | c | 15898 | 16764 58762 | 13176 11930 960744 80.5 | 0.248 % | c | 19743 | 16764 58762 | 14493 9082 663465 73.1 | 0.248 % | c | 25509 | 16764 58762 | 15943 7495 467701 62.4 | 0.248 % | c | 34158 | 16764 58762 | 17537 8088 465515 57.6 | 0.248 % | c ============================================================================== c [1mFound solution: 377[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 431 bits: 10/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36290 | 16765 58769 | 5588 10220 596625 58.4 | 0.248 % | c | 36390 | 16765 58769 | 6146 5210 265803 51.0 | 0.289 % | c | 36543 | 16765 58769 | 6761 5363 270754 50.5 | 0.289 % | c | 36768 | 16765 58769 | 7437 5588 282054 50.5 | 0.289 % | c | 37108 | 16765 58769 | 8181 5928 305263 51.5 | 0.289 % | c | 37617 | 16765 58769 | 8999 6437 348358 54.1 | 0.289 % | c | 38376 | 16765 58769 | 9899 7196 413791 57.5 | 0.289 % | c | 39516 | 16765 58769 | 10889 8336 511333 61.3 | 0.289 % | c | 41225 | 16765 58769 | 11978 10045 652268 64.9 | 0.289 % | c | 43790 | 16765 58769 | 13176 6467 406967 62.9 | 0.289 % | c | 47634 | 16765 58769 | 14493 10311 681211 66.1 | 0.289 % | c | 53401 | 16765 58769 | 15943 8635 464783 53.8 | 0.289 % | c | 62050 | 16765 58769 | 17537 17284 1648697 95.4 | 0.289 % | c | 75024 | 16765 58769 | 19291 12409 693478 55.9 | 0.289 % | c | 94485 | 16765 58769 | 21220 11530 1147320 99.5 | 0.289 % | c | 123677 | 16765 58769 | 23342 19253 1199204 62.3 | 0.289 % | c | 167466 | 16765 58769 | 25676 13548 1632045 120.5 | 0.290 % | c | 233150 | 16765 58769 | 28244 25531 1844859 72.3 | 0.289 % | c | 331676 | 16765 58769 | 31068 16685 1716947 102.9 | 0.289 % | c | 479466 | 16765 58769 | 34175 22850 3230172 141.4 | 0.289 % | c c *** TERMINATED *** s SATISFIABLE v x1 -x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 x11 -x12 -x13 x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 -x41 x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 -x87 x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 -x173 x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 -x187 x188 x189 -x190 -x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 -x219 x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 -x243 x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 x261 -x262 x263 -x264 x265 -x266 -x267 x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 -x289 x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 x321 -x322 x323 -x324 x325 -x326 x327 -x328 x329 -x330 x331 -x332 -x333 x334 x335 -x336 x337 -x338 x339 -x340 x341 -x342 x343 -x344 x345 -x346 x347 -x348 x349 -x350 x351 -x352 x353 -x354 x355 -x356 x357 -x358 x359 -x360 x361 -x362 x363 -x364 x365 -x366 x367 -x368 x369 -x370 x371 -x372 x373 -x374 x375 -x376 x377 -x378 x379 -x380 x381 -x382 x383 -x384 x385 -x386 -x387 -x388 -x389 x390 x391 -x392 -x393 -x394 x395 -x396 x397 -x398 -x399 -x400 -x401 -x402 x403 -x404 -x405 -x406 x407 -x408 x409 -x410 -x411 -x412 x413 -x414 -x415 -x416 x417 -x418 -x419 -x420 -x421 -x422 x423 -x424 -x425 -x426 x427 -x428 -x429 x430 x431 -x432 -x433 -x434 x435 -x436 -x437 -x438 x439 -x440 x441 -x442 -x443 -x444 x445 -x446 x447 -x448 -x449 -x450 x451 -x452 -x453 -x454 x455 -x456 -x457 -x458 x459 -x460 x461 -x462 -x463 x464 x465 -x466 x467 -x468 x469 -x470 -x471 x472 -x473 -x474 x475 -x476 x477 -x478 -x479 x480 x481 -x482 -x483 -x484 x485 -x486 -x487 -x488 x489 -x490 -x491 -x492 x493 -x494 -x495 -x496 x497 -x498 -x499 -x500 x501 -x502 -x503 -x504 x505 -x506 -x507 -x508 x509 -x510 -x511 -x512 -x513 x514 -x515 x516 x517 -x518 -x519 x520 -x521 x522 x523 -x524 -x525 x526 -x527 x528 x529 -x530 -x531 x532 -x533 x534 -x535 x536 -x537 x538 -x539 x540 x541 -x542 -x543 x544 x545 -x546 -x547 x548 -x549 x550 -x551 x552 -x553 x554 -x555 x556 x557 -x558 -x559 x560 -x561 x562 -x563 x564 x565 -x566 -x567 x568 -x569 x570 -x571 x572 x573 -x574 -x575 x576 x577 -x578 -x579 x580 -x581 x582 -x583 x584 -x585 x586 x587 -x588 -x589 x590 -x591 x592 -x593 x594 -x595 x596 x597 -x598 -x599 x600 -x601 x602 -x603 x604 x605 -x606 -x607 x608 -x609 x610 -x611 x612 -x613 x614 x615 -x616 x617 -x618 -x619 x620 -x621 x622 -x623 x624 x625 -x626 -x627 x628 -x629 x630 -x631 x632 -x633 x634 -x635 x636 x637 -x638 -x639 x640 x641 -x642 -x643 x644 -x645 x646 -x647 x648 -x649 x650 -x651 x652 x653 -x654 -x655 x656 -x657 x658 -x659 x660 x661 -x662 -x663 x664 x665 -x666 -x667 x668 -x669 x670 -x671 x672 x673 -x674 -x675 x676 -x677 x678 -x679 x680 -x681 x682 -x683 x684 x685 -x686 -x687 x688 -x689 x690 -x691 x692 x693 -x694 -x695 x696 -x697 x698 -x699 x700 x701 -x702 -x703 x704 x705 -x706 -x707 x708 -x709 x710 -x711 x712 -x713 x714 -x715 x716 x717 -x718 -x719 x720 x721 -x722 -x723 x724 -x725 x726 -x727 x728 -x729 x730 x731 -x732 -x733 x734 -x735 x736 -x737 x738 -x739 x740 x741 -x742 -x743 x744 -x745 x746 x747 -x748 -x749 x750 -x751 x752 -x#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.97 0.88 2/54 28435 Raw data (stat): 28435 (runsolver) R 28434 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 406904130 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0011 s] Raw data (loadavg): 0.93 0.97 0.88 2/54 28435 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 1462 0 0 0 994 4 0 0 25 0 1 0 406904130 7593984 1440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1854 1440 603 41 0 1813 0 vsize: 7416 [startup+20.0018 s] Raw data (loadavg): 0.94 0.97 0.88 2/54 28435 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 1946 0 0 0 1991 6 0 0 25 0 1 0 406904130 9617408 1924 4294967295 134512640 134672761 3221224576 3221223760 134559365 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2348 1924 603 41 0 2307 0 vsize: 9392 [startup+30.0013 s] Raw data (loadavg): 0.95 0.97 0.88 2/54 28435 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 1990 0 0 0 2991 6 0 0 25 0 1 0 406904130 9752576 1968 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2381 1968 603 41 0 2340 0 vsize: 9524 [startup+40.0014 s] Raw data (loadavg): 0.96 0.97 0.88 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 2038 0 0 0 3991 7 0 0 25 0 1 0 406904130 10022912 2016 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2447 2016 603 41 0 2406 0 vsize: 9788 [startup+50.0022 s] Raw data (loadavg): 0.96 0.97 0.88 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 2100 0 0 0 4990 7 0 0 25 0 1 0 406904130 10293248 2078 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2513 2078 603 41 0 2472 0 vsize: 10052 [startup+60.0026 s] Raw data (loadavg): 0.97 0.97 0.88 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 2100 0 0 0 5990 7 0 0 25 0 1 0 406904130 10293248 2078 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2513 2078 603 41 0 2472 0 vsize: 10052 [startup+70.0027 s] Raw data (loadavg): 0.97 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 2184 0 0 0 6991 7 0 0 25 0 1 0 406904130 10694656 2162 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2611 2162 603 41 0 2570 0 vsize: 10444 [startup+80.0025 s] Raw data (loadavg): 0.98 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 2844 0 0 0 7989 8 0 0 25 0 1 0 406904130 13361152 2822 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3262 2822 603 41 0 3221 0 vsize: 13048 [startup+90.003 s] Raw data (loadavg): 0.98 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 2867 0 0 0 8990 8 0 0 25 0 1 0 406904130 13500416 2845 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3296 2845 603 41 0 3255 0 vsize: 13184 [startup+100.003 s] Raw data (loadavg): 0.98 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 2869 0 0 0 9990 8 0 0 25 0 1 0 406904130 13500416 2847 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3296 2847 603 41 0 3255 0 vsize: 13184 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3020 0 0 0 10990 9 0 0 25 0 1 0 406904130 14172160 2998 4294967295 134512640 134672761 3221224576 3221223680 134560318 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3460 2998 603 41 0 3419 0 vsize: 13840 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3067 0 0 0 11990 9 0 0 25 0 1 0 406904130 14311424 3045 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3494 3045 603 41 0 3453 0 vsize: 13976 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3074 0 0 0 12990 9 0 0 25 0 1 0 406904130 14311424 3052 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3494 3052 603 41 0 3453 0 vsize: 13976 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3074 0 0 0 13990 9 0 0 25 0 1 0 406904130 14311424 3052 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3494 3052 603 41 0 3453 0 vsize: 13976 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3107 0 0 0 14990 9 0 0 25 0 1 0 406904130 14446592 3085 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3527 3085 603 41 0 3486 0 vsize: 14108 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.89 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3473 0 0 0 15989 10 0 0 25 0 1 0 406904130 15929344 3451 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3889 3451 603 41 0 3848 0 vsize: 15556 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3999 0 0 0 16988 11 0 0 25 0 1 0 406904130 18079744 3977 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4414 3977 603 41 0 4373 0 vsize: 17656 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 3999 0 0 0 17988 11 0 0 25 0 1 0 406904130 18079744 3977 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4414 3977 603 41 0 4373 0 vsize: 17656 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4325 0 0 0 18988 12 0 0 25 0 1 0 406904130 19427328 4303 4294967295 134512640 134672761 3221224576 3221223760 134559583 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4743 4303 603 41 0 4702 0 vsize: 18972 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4325 0 0 0 19988 12 0 0 25 0 1 0 406904130 19427328 4303 4294967295 134512640 134672761 3221224576 3221223680 134559814 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4743 4303 603 41 0 4702 0 vsize: 18972 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4325 0 0 0 20988 12 0 0 25 0 1 0 406904130 19427328 4303 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4743 4303 603 41 0 4702 0 vsize: 18972 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4793 0 0 0 21987 13 0 0 25 0 1 0 406904130 21315584 4771 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4771 603 41 0 5163 0 vsize: 20816 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4796 0 0 0 22987 13 0 0 25 0 1 0 406904130 21315584 4774 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4774 603 41 0 5163 0 vsize: 20816 [startup+240.008 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4797 0 0 0 23988 13 0 0 25 0 1 0 406904130 21315584 4775 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4775 603 41 0 5163 0 vsize: 20816 [startup+250.008 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4798 0 0 0 24988 13 0 0 25 0 1 0 406904130 21315584 4776 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4776 603 41 0 5163 0 vsize: 20816 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.90 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4799 0 0 0 25988 13 0 0 25 0 1 0 406904130 21315584 4777 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4777 603 41 0 5163 0 vsize: 20816 [startup+270.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4801 0 0 0 26988 13 0 0 25 0 1 0 406904130 21315584 4779 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4779 603 41 0 5163 0 vsize: 20816 [startup+280.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4803 0 0 0 27988 13 0 0 25 0 1 0 406904130 21315584 4781 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4781 603 41 0 5163 0 vsize: 20816 [startup+290.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4803 0 0 0 28989 13 0 0 25 0 1 0 406904130 21315584 4781 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4781 603 41 0 5163 0 vsize: 20816 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4804 0 0 0 29989 13 0 0 25 0 1 0 406904130 21315584 4782 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4782 603 41 0 5163 0 vsize: 20816 [startup+310.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4804 0 0 0 30989 13 0 0 25 0 1 0 406904130 21315584 4782 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4782 603 41 0 5163 0 vsize: 20816 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4805 0 0 0 31988 14 0 0 25 0 1 0 406904130 21315584 4783 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5204 4783 603 41 0 5163 0 vsize: 20816 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4805 0 0 0 32987 14 0 0 25 0 1 0 406904130 21315584 4783 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4783 603 41 0 5163 0 vsize: 20816 [startup+340.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4805 0 0 0 33987 14 0 0 25 0 1 0 406904130 21315584 4783 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4783 603 41 0 5163 0 vsize: 20816 [startup+350.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4805 0 0 0 34988 14 0 0 25 0 1 0 406904130 21315584 4783 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4783 603 41 0 5163 0 vsize: 20816 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4805 0 0 0 35988 14 0 0 25 0 1 0 406904130 21315584 4783 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4783 603 41 0 5163 0 vsize: 20816 [startup+370.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4806 0 0 0 36988 14 0 0 25 0 1 0 406904130 21315584 4784 4294967295 134512640 134672761 3221224576 3221223592 1075353072 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4784 603 41 0 5163 0 vsize: 20816 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 4806 0 0 0 37988 14 0 0 25 0 1 0 406904130 21315584 4784 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5204 4784 603 41 0 5163 0 vsize: 20816 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 5125 0 0 0 38987 15 0 0 25 0 1 0 406904130 22650880 5103 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5530 5103 603 41 0 5489 0 vsize: 22120 [startup+400.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 5875 0 0 0 39986 16 0 0 25 0 1 0 406904130 25747456 5853 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6286 5853 603 41 0 6245 0 vsize: 25144 [startup+410.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 5985 0 0 0 40986 17 0 0 25 0 1 0 406904130 26152960 5963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6385 5963 603 41 0 6344 0 vsize: 25540 [startup+420.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 5985 0 0 0 41986 17 0 0 25 0 1 0 406904130 26152960 5963 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6385 5963 603 41 0 6344 0 vsize: 25540 [startup+430.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 6036 0 0 0 42986 17 0 0 25 0 1 0 406904130 26423296 6014 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6451 6014 603 41 0 6410 0 vsize: 25804 [startup+440.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 6704 0 0 0 43984 20 0 0 25 0 1 0 406904130 29147136 6682 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7116 6682 603 41 0 7075 0 vsize: 28464 [startup+450.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7162 0 0 0 44983 21 0 0 25 0 1 0 406904130 31031296 7140 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7140 603 41 0 7535 0 vsize: 30304 [startup+460.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7163 0 0 0 45983 21 0 0 25 0 1 0 406904130 31031296 7141 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7141 603 41 0 7535 0 vsize: 30304 [startup+470.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7163 0 0 0 46983 21 0 0 25 0 1 0 406904130 31031296 7141 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7141 603 41 0 7535 0 vsize: 30304 [startup+480.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7164 0 0 0 47983 21 0 0 25 0 1 0 406904130 31031296 7142 4294967295 134512640 134672761 3221224576 3221223736 134560076 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7142 603 41 0 7535 0 vsize: 30304 [startup+490.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7164 0 0 0 48983 21 0 0 25 0 1 0 406904130 31031296 7142 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7142 603 41 0 7535 0 vsize: 30304 [startup+500.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7164 0 0 0 49984 21 0 0 25 0 1 0 406904130 31031296 7142 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7142 603 41 0 7535 0 vsize: 30304 [startup+510.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7164 0 0 0 50983 21 0 0 25 0 1 0 406904130 31031296 7142 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7142 603 41 0 7535 0 vsize: 30304 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7164 0 0 0 51983 21 0 0 25 0 1 0 406904130 31031296 7142 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7576 7142 603 41 0 7535 0 vsize: 30304 [startup+530.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 52983 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+540.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 53983 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+550.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 54984 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+560.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 55984 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+570.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 56984 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+580.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 57984 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223700 134566031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+590.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 58985 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+600.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 59985 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+610.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 60985 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+620.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 61985 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+630.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 62985 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+640.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 63986 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+650.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 64986 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+660.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 65986 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+670.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 66986 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+680.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 67986 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+690.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 68987 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223680 134560306 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+700.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 69987 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+710.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 70987 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+720.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 71987 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+730.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 72987 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+740.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 73988 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+750.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 74988 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+760.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 75988 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+770.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 76988 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+780.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 77988 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+790.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 78989 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+800.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 79989 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+810.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7198 0 0 0 80989 21 0 0 25 0 1 0 406904130 31232000 7175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7625 7175 603 41 0 7584 0 vsize: 30500 [startup+820.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 81989 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+830.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 82989 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+840.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 83989 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+850.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 84989 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+860.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 85990 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+870.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 86990 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223680 134560279 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+880.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 87990 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+890.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7348 0 0 0 88989 21 0 0 25 0 1 0 406904130 31903744 7325 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7325 603 41 0 7748 0 vsize: 31156 [startup+900.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 89989 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223680 134560350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+910.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 90989 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+920.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 91989 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+930.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 92990 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+940.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 93990 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+950.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 94990 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223760 134559199 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+960.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 95990 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+970.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7351 0 0 0 96990 21 0 0 25 0 1 0 406904130 31903744 7328 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7789 7328 603 41 0 7748 0 vsize: 31156 [startup+980.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 7461 0 0 0 97990 22 0 0 25 0 1 0 406904130 32440320 7438 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7920 7438 603 41 0 7879 0 vsize: 31680 [startup+990.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8005 0 0 0 98989 23 0 0 25 0 1 0 406904130 34594816 7982 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8446 7982 603 41 0 8405 0 vsize: 33784 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8373 0 0 0 99988 24 0 0 25 0 1 0 406904130 36057088 8350 4294967295 134512640 134672761 3221224576 3221223744 134560836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8803 8350 603 41 0 8762 0 vsize: 35212 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8373 0 0 0 100988 24 0 0 25 0 1 0 406904130 36057088 8350 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8803 8350 603 41 0 8762 0 vsize: 35212 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8373 0 0 0 101989 24 0 0 25 0 1 0 406904130 36057088 8350 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8803 8350 603 41 0 8762 0 vsize: 35212 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8373 0 0 0 102989 24 0 0 25 0 1 0 406904130 36057088 8350 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8803 8350 603 41 0 8762 0 vsize: 35212 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8373 0 0 0 103989 24 0 0 25 0 1 0 406904130 36057088 8350 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8803 8350 603 41 0 8762 0 vsize: 35212 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8441 0 0 0 104989 24 0 0 25 0 1 0 406904130 36458496 8418 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8901 8418 603 41 0 8860 0 vsize: 35604 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8984 0 0 0 105988 26 0 0 25 0 1 0 406904130 38612992 8961 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8961 603 41 0 9386 0 vsize: 37708 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8984 0 0 0 106988 26 0 0 25 0 1 0 406904130 38612992 8961 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8961 603 41 0 9386 0 vsize: 37708 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8984 0 0 0 107988 26 0 0 25 0 1 0 406904130 38612992 8961 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8961 603 41 0 9386 0 vsize: 37708 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 108989 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 109989 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 110989 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 111989 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 112989 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 113989 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 114990 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223680 134560355 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 115990 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 116990 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 117990 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 118990 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28437 Raw data (stat): 28435 (minisat+) R 28434 26667 26666 0 -1 0 8985 0 0 0 119991 26 0 0 25 0 1 0 406904130 38612992 8962 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9427 8962 603 41 0 9386 0 vsize: 37708 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 28437 Raw data (stat): 28435 (minisat+) Z 28434 26667 26666 0 -1 12 8988 0 0 0 119991 28 0 0 25 0 1 0 406904130 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.05 CPU time (s): 1200.19 CPU user time (s): 1199.91 CPU system time (s): 0.281957 CPU usage (%): 100.012 Max. virtual memory (Kb): 37708 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####