Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a4.opb |
MD5SUM | 8a77190c2eeefb9e88447a9087adfd6f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 283 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 792 |
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 | 792 |
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 | 792 |
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.02084 |
Number of variables | 792 |
Total number of constraints | 3194 |
Number of constraints which are clauses | 3194 |
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 | 8 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-04-13 20:50:21 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=1490 boxname=wulflinc19 idbench=166 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 8a77190c2eeefb9e88447a9087adfd6f /oldhome/oroussel/tmp/wulflinc19/normalized-ii8a4.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc19/normalized-ii8a4.opb IDLAUNCH: 1490 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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: 893696 kB Buffers: 33424 kB Cached: 74028 kB SwapCached: 56 kB Active: 45160 kB Inactive: 65256 kB HighTotal: 131008 kB HighFree: 53004 kB LowTotal: 903652 kB LowFree: 840692 kB SwapTotal: 2097892 kB SwapFree: 2097836 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7028 kB Slab: 24984 kB Committed_AS: 63708 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 21:10:23 (client local time) WITH STATUS 10 IN 1200.23 SECONDS stats: 1490 7 1200.23 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 3194 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 | 3194 8388 | 1064 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 354[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:36470 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4 | 47626 112246 | 15875 4 26 6.5 | 0.000 % | c | 104 | 47361 111687 | 17462 93 1225 13.2 | 0.521 % | c | 254 | 47361 111687 | 19208 243 4630 19.1 | 0.521 % | c ============================================================================== c [1mFound solution: 346[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 431 | 47442 111960 | 15814 419 7912 18.9 | 0.521 % | c | 533 | 47360 111784 | 17395 519 11037 21.3 | 0.777 % | c ============================================================================== c [1mFound solution: 319[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 582 | 47671 112647 | 15890 567 12211 21.5 | 0.777 % | c | 682 | 47671 112647 | 17479 667 13724 20.6 | 0.860 % | c | 834 | 47671 112647 | 19226 819 15865 19.4 | 0.860 % | c | 1060 | 47629 112553 | 21149 1044 23666 22.7 | 0.945 % | c | 1397 | 46908 110974 | 23264 1363 35493 26.0 | 2.354 % | c | 1903 | 46287 109586 | 25591 1851 65230 35.2 | 3.588 % | c ============================================================================== c [1mFound solution: 294[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2040 | 46486 110113 | 15495 1975 65744 33.3 | 3.588 % | c | 2141 | 46486 110113 | 17044 2076 68018 32.8 | 3.771 % | c | 2292 | 46486 110113 | 18748 2227 72609 32.6 | 3.771 % | c | 2518 | 46433 109991 | 20623 2452 84110 34.3 | 3.882 % | c | 2857 | 46312 109724 | 22686 2785 100451 36.1 | 4.120 % | c | 3365 | 46312 109724 | 24954 3293 114048 34.6 | 4.120 % | c ============================================================================== c [1mFound solution: 283[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3625 | 46434 110062 | 15478 3553 118845 33.4 | 4.120 % | c | 3725 | 46354 109900 | 17025 3649 124499 34.1 | 4.296 % | c | 3875 | 46354 109900 | 18728 3799 129147 34.0 | 4.296 % | c | 4100 | 46264 109704 | 20601 4022 140449 34.9 | 4.469 % | c | 4437 | 45953 109018 | 22661 4287 150386 35.1 | 5.077 % | c | 4943 | 45894 108887 | 24927 4792 219227 45.7 | 5.194 % | c | 5702 | 45382 107757 | 27420 5532 256414 46.4 | 6.189 % | c | 6841 | 45339 107666 | 30162 6668 364309 54.6 | 6.267 % | c | 8549 | 45288 107557 | 33178 8373 491019 58.6 | 6.362 % | c | 11112 | 45168 107273 | 36496 10923 611414 56.0 | 6.622 % | c | 14956 | 45122 107167 | 40145 14759 795096 53.9 | 6.719 % | c | 20724 | 45026 106949 | 44160 20508 1308058 63.8 | 6.918 % | c | 29373 | 45026 106949 | 48576 29157 2150568 73.8 | 6.918 % | c | 42347 | 45026 106949 | 53434 42131 2922952 69.4 | 6.918 % | c | 61808 | 45000 106891 | 58777 21517 1280796 59.5 | 6.970 % | c | 91000 | 44991 106872 | 64655 50708 3380801 66.7 | 6.986 % | c | 134789 | 44882 106619 | 71120 46306 3138339 67.8 | 7.220 % | c | 200473 | 44882 106619 | 78233 57666 3417826 59.3 | 7.220 % | 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#### 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.91 0.95 0.90 2/55 25760 Raw data (stat): 25760 (runsolver) R 25759 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478958823 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0001 s] Raw data (loadavg): 0.93 0.95 0.90 2/55 25760 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 2817 0 0 0 992 6 0 0 25 0 1 0 478958823 13676544 2742 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3339 2742 603 41 0 3298 0 vsize: 13356 [startup+20.0006 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 25760 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3088 0 0 0 1991 7 0 0 25 0 1 0 478958823 14884864 3013 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3634 3013 603 41 0 3593 0 vsize: 14536 [startup+30.0012 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 25760 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3354 0 0 0 2989 8 0 0 25 0 1 0 478958823 16003072 3279 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3907 3279 603 41 0 3866 0 vsize: 15628 [startup+40.0021 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 25760 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3595 0 0 0 3988 9 0 0 25 0 1 0 478958823 16936960 3520 4294967295 134512640 134672761 3221224640 3221223776 134565076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4135 3520 603 41 0 4094 0 vsize: 16540 [startup+50.0026 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 25760 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3870 0 0 0 4988 10 0 0 25 0 1 0 478958823 18141184 3795 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4429 3795 603 41 0 4388 0 vsize: 17716 [startup+60.0025 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 4147 0 0 0 5987 11 0 0 25 0 1 0 478958823 19210240 4072 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4690 4072 603 41 0 4649 0 vsize: 18760 [startup+70.0035 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 4526 0 0 0 6986 12 0 0 25 0 1 0 478958823 20819968 4451 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5083 4451 603 41 0 5042 0 vsize: 20332 [startup+80.0041 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 4798 0 0 0 7986 13 0 0 25 0 1 0 478958823 21880832 4723 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5342 4723 603 41 0 5301 0 vsize: 21368 [startup+90.0049 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5057 0 0 0 8985 13 0 0 25 0 1 0 478958823 22929408 4982 4294967295 134512640 134672761 3221224640 3221223824 134559514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5598 4982 603 41 0 5557 0 vsize: 22392 [startup+100.005 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5288 0 0 0 9985 14 0 0 25 0 1 0 478958823 23859200 5213 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5825 5213 603 41 0 5784 0 vsize: 23300 [startup+110.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5494 0 0 0 10985 14 0 0 25 0 1 0 478958823 24776704 5419 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6049 5419 603 41 0 6008 0 vsize: 24196 [startup+120.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5686 0 0 0 11984 15 0 0 25 0 1 0 478958823 25575424 5611 4294967295 134512640 134672761 3221224640 3221223824 134559199 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6244 5611 603 41 0 6203 0 vsize: 24976 [startup+130.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5859 0 0 0 12983 16 0 0 25 0 1 0 478958823 26247168 5784 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6408 5784 603 41 0 6367 0 vsize: 25632 [startup+140.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6066 0 0 0 13983 16 0 0 25 0 1 0 478958823 27185152 5991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6637 5991 603 41 0 6596 0 vsize: 26548 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6285 0 0 0 14983 17 0 0 25 0 1 0 478958823 27983872 6210 4294967295 134512640 134672761 3221224640 3221223744 134555211 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6832 6210 603 41 0 6791 0 vsize: 27328 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6463 0 0 0 15982 18 0 0 25 0 1 0 478958823 28774400 6388 4294967295 134512640 134672761 3221224640 3221223744 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7025 6388 603 41 0 6984 0 vsize: 28100 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6646 0 0 0 16982 18 0 0 25 0 1 0 478958823 29446144 6571 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7189 6571 603 41 0 7148 0 vsize: 28756 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6862 0 0 0 17982 18 0 0 25 0 1 0 478958823 30375936 6787 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7416 6787 603 41 0 7375 0 vsize: 29664 [startup+190.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7057 0 0 0 18981 19 0 0 25 0 1 0 478958823 31174656 6982 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7611 6982 603 41 0 7570 0 vsize: 30444 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7264 0 0 0 19981 20 0 0 25 0 1 0 478958823 31965184 7189 4294967295 134512640 134672761 3221224640 3221223700 1075346557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7804 7189 603 41 0 7763 0 vsize: 31216 [startup+210.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7449 0 0 0 20981 20 0 0 25 0 1 0 478958823 32763904 7374 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7999 7374 603 41 0 7958 0 vsize: 31996 [startup+220.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7608 0 0 0 21980 20 0 0 25 0 1 0 478958823 33419264 7533 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8159 7533 603 41 0 8118 0 vsize: 32636 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7758 0 0 0 22980 21 0 0 25 0 1 0 478958823 34074624 7683 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7683 603 41 0 8278 0 vsize: 33276 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 23980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7685 603 41 0 8278 0 vsize: 33276 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 24980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7685 603 41 0 8278 0 vsize: 33276 [startup+260.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 25980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223744 134560198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7685 603 41 0 8278 0 vsize: 33276 [startup+270.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 26980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7685 603 41 0 8278 0 vsize: 33276 [startup+280.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7765 0 0 0 27981 21 0 0 25 0 1 0 478958823 34074624 7690 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7690 603 41 0 8278 0 vsize: 33276 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7766 0 0 0 28981 21 0 0 25 0 1 0 478958823 34074624 7691 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7691 603 41 0 8278 0 vsize: 33276 [startup+300.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7767 0 0 0 29981 21 0 0 25 0 1 0 478958823 34074624 7692 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7692 603 41 0 8278 0 vsize: 33276 [startup+310.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7767 0 0 0 30981 21 0 0 25 0 1 0 478958823 34074624 7692 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7692 603 41 0 8278 0 vsize: 33276 [startup+320.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7772 0 0 0 31981 21 0 0 25 0 1 0 478958823 34074624 7697 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7697 603 41 0 8278 0 vsize: 33276 [startup+330.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7773 0 0 0 32981 21 0 0 25 0 1 0 478958823 34074624 7698 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7698 603 41 0 8278 0 vsize: 33276 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7779 0 0 0 33981 21 0 0 25 0 1 0 478958823 34074624 7704 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7704 603 41 0 8278 0 vsize: 33276 [startup+350.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25762 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7780 0 0 0 34982 21 0 0 25 0 1 0 478958823 34074624 7705 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8319 7705 603 41 0 8278 0 vsize: 33276 [startup+360.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7786 0 0 0 35982 21 0 0 25 0 1 0 478958823 34213888 7711 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8353 7711 603 41 0 8312 0 vsize: 33412 [startup+370.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7786 0 0 0 36981 21 0 0 25 0 1 0 478958823 34213888 7711 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8353 7711 603 41 0 8312 0 vsize: 33412 [startup+380.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7805 0 0 0 37981 22 0 0 25 0 1 0 478958823 34213888 7730 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8353 7730 603 41 0 8312 0 vsize: 33412 [startup+390.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7817 0 0 0 38982 22 0 0 25 0 1 0 478958823 34377728 7742 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8393 7742 603 41 0 8352 0 vsize: 33572 [startup+400.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7818 0 0 0 39982 22 0 0 25 0 1 0 478958823 34377728 7743 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8393 7743 603 41 0 8352 0 vsize: 33572 [startup+410.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7818 0 0 0 40982 22 0 0 25 0 1 0 478958823 34377728 7743 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8393 7743 603 41 0 8352 0 vsize: 33572 [startup+420.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7819 0 0 0 41982 22 0 0 25 0 1 0 478958823 34377728 7744 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8393 7744 603 41 0 8352 0 vsize: 33572 [startup+430.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7822 0 0 0 42982 22 0 0 25 0 1 0 478958823 34377728 7747 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8393 7747 603 41 0 8352 0 vsize: 33572 [startup+440.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7953 0 0 0 43982 22 0 0 25 0 1 0 478958823 34906112 7878 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8522 7878 603 41 0 8481 0 vsize: 34088 [startup+450.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8101 0 0 0 44982 23 0 0 25 0 1 0 478958823 35438592 8026 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8652 8026 603 41 0 8611 0 vsize: 34608 [startup+460.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8243 0 0 0 45982 23 0 0 25 0 1 0 478958823 36233216 8168 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8846 8168 603 41 0 8805 0 vsize: 35384 [startup+470.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8377 0 0 0 46981 24 0 0 25 0 1 0 478958823 36888576 8302 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9006 8302 603 41 0 8965 0 vsize: 36024 [startup+480.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8467 0 0 0 47981 24 0 0 25 0 1 0 478958823 37158912 8392 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9072 8392 603 41 0 9031 0 vsize: 36288 [startup+490.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8467 0 0 0 48981 24 0 0 25 0 1 0 478958823 37158912 8392 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9072 8392 603 41 0 9031 0 vsize: 36288 [startup+500.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8477 0 0 0 49981 24 0 0 25 0 1 0 478958823 37318656 8402 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8402 603 41 0 9070 0 vsize: 36444 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8478 0 0 0 50981 24 0 0 25 0 1 0 478958823 37318656 8403 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8403 603 41 0 9070 0 vsize: 36444 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8478 0 0 0 51982 24 0 0 25 0 1 0 478958823 37318656 8403 4294967295 134512640 134672761 3221224640 3221223792 134541817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8403 603 41 0 9070 0 vsize: 36444 [startup+530.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8479 0 0 0 52982 24 0 0 25 0 1 0 478958823 37318656 8404 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8404 603 41 0 9070 0 vsize: 36444 [startup+540.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8479 0 0 0 53982 24 0 0 25 0 1 0 478958823 37318656 8404 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8404 603 41 0 9070 0 vsize: 36444 [startup+550.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8479 0 0 0 54982 24 0 0 25 0 1 0 478958823 37318656 8404 4294967295 134512640 134672761 3221224640 3221223824 134559291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8404 603 41 0 9070 0 vsize: 36444 [startup+560.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8485 0 0 0 55982 24 0 0 25 0 1 0 478958823 37318656 8410 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8410 603 41 0 9070 0 vsize: 36444 [startup+570.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8486 0 0 0 56982 24 0 0 25 0 1 0 478958823 37318656 8411 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8411 603 41 0 9070 0 vsize: 36444 [startup+580.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 25764 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8486 0 0 0 57985 24 0 0 25 0 1 0 478958823 37318656 8411 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8411 603 41 0 9070 0 vsize: 36444 [startup+590.037 s] Raw data (loadavg): 1.07 0.99 0.91 2/55 25817 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8486 0 0 0 58984 24 0 0 25 0 1 0 478958823 37318656 8411 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8411 603 41 0 9070 0 vsize: 36444 [startup+600.037 s] Raw data (loadavg): 1.06 0.99 0.91 2/55 25817 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8487 0 0 0 59985 24 0 0 25 0 1 0 478958823 37318656 8412 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8412 603 41 0 9070 0 vsize: 36444 [startup+610.037 s] Raw data (loadavg): 1.05 0.99 0.91 2/55 25817 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8492 0 0 0 60984 25 0 0 25 0 1 0 478958823 37318656 8417 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8417 603 41 0 9070 0 vsize: 36444 [startup+620.038 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 25817 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8505 0 0 0 61984 25 0 0 25 0 1 0 478958823 37482496 8430 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8430 603 41 0 9110 0 vsize: 36604 [startup+630.037 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 25817 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8516 0 0 0 62985 25 0 0 25 0 1 0 478958823 37482496 8441 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8441 603 41 0 9110 0 vsize: 36604 [startup+640.038 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 25817 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8519 0 0 0 63985 25 0 0 25 0 1 0 478958823 37482496 8444 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8444 603 41 0 9110 0 vsize: 36604 [startup+650.038 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 25817 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8521 0 0 0 64985 25 0 0 25 0 1 0 478958823 37482496 8446 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8446 603 41 0 9110 0 vsize: 36604 [startup+660.038 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8521 0 0 0 65985 25 0 0 25 0 1 0 478958823 37482496 8446 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8446 603 41 0 9110 0 vsize: 36604 [startup+670.038 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8522 0 0 0 66985 25 0 0 25 0 1 0 478958823 37482496 8447 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8447 603 41 0 9110 0 vsize: 36604 [startup+680.039 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8523 0 0 0 67985 25 0 0 25 0 1 0 478958823 37482496 8448 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8448 603 41 0 9110 0 vsize: 36604 [startup+690.039 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8524 0 0 0 68986 25 0 0 25 0 1 0 478958823 37482496 8449 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8449 603 41 0 9110 0 vsize: 36604 [startup+700.039 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8552 0 0 0 69986 25 0 0 25 0 1 0 478958823 37679104 8477 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8477 603 41 0 9158 0 vsize: 36796 [startup+710.039 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8562 0 0 0 70986 25 0 0 25 0 1 0 478958823 37871616 8487 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9246 8487 603 41 0 9205 0 vsize: 36984 [startup+720.039 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8565 0 0 0 71986 25 0 0 25 0 1 0 478958823 37871616 8490 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9246 8490 603 41 0 9205 0 vsize: 36984 [startup+730.04 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8593 0 0 0 72986 25 0 0 25 0 1 0 478958823 37871616 8518 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9246 8518 603 41 0 9205 0 vsize: 36984 [startup+740.04 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8600 0 0 0 73986 25 0 0 25 0 1 0 478958823 38068224 8525 4294967295 134512640 134672761 3221224640 3221223824 134558883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9294 8525 603 41 0 9253 0 vsize: 37176 [startup+750.04 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8709 0 0 0 74986 25 0 0 25 0 1 0 478958823 38461440 8634 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9390 8634 603 41 0 9349 0 vsize: 37560 [startup+760.04 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8837 0 0 0 75986 26 0 0 25 0 1 0 478958823 38989824 8762 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9519 8762 603 41 0 9478 0 vsize: 38076 [startup+770.041 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8955 0 0 0 76985 27 0 0 25 0 1 0 478958823 39391232 8880 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9617 8880 603 41 0 9576 0 vsize: 38468 [startup+780.041 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9075 0 0 0 77985 27 0 0 25 0 1 0 478958823 39919616 9000 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9746 9000 603 41 0 9705 0 vsize: 38984 [startup+790.042 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9138 0 0 0 78985 27 0 0 25 0 1 0 478958823 40181760 9063 4294967295 134512640 134672761 3221224640 3221223744 134560399 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9063 603 41 0 9769 0 vsize: 39240 [startup+800.042 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9138 0 0 0 79986 27 0 0 25 0 1 0 478958823 40181760 9063 4294967295 134512640 134672761 3221224640 3221223824 134558423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9063 603 41 0 9769 0 vsize: 39240 [startup+810.042 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9138 0 0 0 80986 27 0 0 25 0 1 0 478958823 40181760 9063 4294967295 134512640 134672761 3221224640 3221223744 134560171 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9063 603 41 0 9769 0 vsize: 39240 [startup+820.042 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9141 0 0 0 81986 27 0 0 25 0 1 0 478958823 40181760 9066 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9066 603 41 0 9769 0 vsize: 39240 [startup+830.042 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9149 0 0 0 82986 27 0 0 25 0 1 0 478958823 40181760 9074 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9074 603 41 0 9769 0 vsize: 39240 [startup+840.042 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9150 0 0 0 83986 27 0 0 25 0 1 0 478958823 40181760 9075 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9075 603 41 0 9769 0 vsize: 39240 [startup+850.043 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 84986 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223736 1075347241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9076 603 41 0 9769 0 vsize: 39240 [startup+860.043 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 85987 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9076 603 41 0 9769 0 vsize: 39240 [startup+870.044 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 86987 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9076 603 41 0 9769 0 vsize: 39240 [startup+880.044 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 87987 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9076 603 41 0 9769 0 vsize: 39240 [startup+890.045 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25821 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9152 0 0 0 88987 27 0 0 25 0 1 0 478958823 40181760 9077 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9077 603 41 0 9769 0 vsize: 39240 [startup+900.045 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25823 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9152 0 0 0 89987 28 0 0 25 0 1 0 478958823 40181760 9077 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9810 9077 603 41 0 9769 0 vsize: 39240 [startup+910.045 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25823 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9157 0 0 0 90987 28 0 0 25 0 1 0 478958823 40316928 9082 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9082 603 41 0 9802 0 vsize: 39372 [startup+920.046 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25823 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9158 0 0 0 91987 28 0 0 25 0 1 0 478958823 40316928 9083 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9083 603 41 0 9802 0 vsize: 39372 [startup+930.045 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25823 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9159 0 0 0 92987 28 0 0 25 0 1 0 478958823 40316928 9084 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9084 603 41 0 9802 0 vsize: 39372 [startup+940.046 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25823 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9169 0 0 0 93988 28 0 0 25 0 1 0 478958823 40316928 9094 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9094 603 41 0 9802 0 vsize: 39372 [startup+950.047 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25823 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 94988 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9095 603 41 0 9802 0 vsize: 39372 [startup+960.046 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 95988 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9095 603 41 0 9802 0 vsize: 39372 [startup+970.046 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 96987 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223744 134560252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9843 9095 603 41 0 9802 0 vsize: 39372 [startup+980.047 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 97987 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9095 603 41 0 9802 0 vsize: 39372 [startup+990.047 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 98987 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9843 9095 603 41 0 9802 0 vsize: 39372 [startup+1000.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9194 0 0 0 99987 28 0 0 25 0 1 0 478958823 40513536 9119 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9119 603 41 0 9850 0 vsize: 39564 [startup+1010.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9196 0 0 0 100987 28 0 0 25 0 1 0 478958823 40513536 9121 4294967295 134512640 134672761 3221224640 3221223800 134561029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9121 603 41 0 9850 0 vsize: 39564 [startup+1020.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9197 0 0 0 101988 28 0 0 25 0 1 0 478958823 40513536 9122 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9122 603 41 0 9850 0 vsize: 39564 [startup+1030.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9197 0 0 0 102988 28 0 0 25 0 1 0 478958823 40513536 9122 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9122 603 41 0 9850 0 vsize: 39564 [startup+1040.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9197 0 0 0 103988 28 0 0 25 0 1 0 478958823 40513536 9122 4294967295 134512640 134672761 3221224640 3221223744 134560215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9122 603 41 0 9850 0 vsize: 39564 [startup+1050.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9198 0 0 0 104988 28 0 0 25 0 1 0 478958823 40513536 9123 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9123 603 41 0 9850 0 vsize: 39564 [startup+1060.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9198 0 0 0 105988 28 0 0 25 0 1 0 478958823 40513536 9123 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9123 603 41 0 9850 0 vsize: 39564 [startup+1070.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9199 0 0 0 106988 29 0 0 25 0 1 0 478958823 40513536 9124 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9124 603 41 0 9850 0 vsize: 39564 [startup+1080.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9201 0 0 0 107989 29 0 0 25 0 1 0 478958823 40513536 9126 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9126 603 41 0 9850 0 vsize: 39564 [startup+1090.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9203 0 0 0 108989 29 0 0 25 0 1 0 478958823 40513536 9128 4294967295 134512640 134672761 3221224640 3221223824 134558848 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9128 603 41 0 9850 0 vsize: 39564 [startup+1100.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 109989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1110.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 110989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1120.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 111989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223744 134560198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1130.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 112989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1140.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 113990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1150.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 114990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223776 134565098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1160.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 115990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1170.05 s] Raw data (loadavg): 1.07 1.00 0.92 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 116990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1180.05 s] Raw data (loadavg): 1.06 1.00 0.92 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 117990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9131 603 41 0 9850 0 vsize: 39564 [startup+1190.06 s] Raw data (loadavg): 1.05 1.00 0.92 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9209 0 0 0 118991 29 0 0 25 0 1 0 478958823 40513536 9134 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9134 603 41 0 9850 0 vsize: 39564 [startup+1200.06 s] Raw data (loadavg): 1.04 1.00 0.92 2/55 25825 Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9209 0 0 0 119991 29 0 0 25 0 1 0 478958823 40513536 9134 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 9134 603 41 0 9850 0 vsize: 39564 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 1.04 1.00 0.92 1/55 25825 Raw data (stat): 25760 (minisat+) Z 25759 22929 22928 0 -1 12 9212 0 0 0 119991 31 0 0 25 0 1 0 478958823 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.08 CPU time (s): 1200.23 CPU user time (s): 1199.92 CPU system time (s): 0.311952 CPU usage (%): 100.012 Max. virtual memory (Kb): 39564 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####