Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-noswot.opb |
MD5SUM | 9b64c494b06e0d267a16a958bcbc40bb |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -41 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 425 |
Biggest coefficient in the objective function | 65536 |
Number of bits for the biggest coefficient in the objective function | 17 |
Sum of the numbers in the objective function | 3276775 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 113777046323200 |
Number of bits of the biggest number in a constraint | 47 |
Biggest sum of numbers in a constraint | 235765682083953 |
Number of bits of the biggest sum of numbers | 48 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 206.622 |
Number of variables | 1060 |
Total number of constraints | 282 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 75 |
Number of constraints which are nor clauses,nor cardinality constraints | 207 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 425 |
LAUNCH ON wulflinc2 THE 2005-09-20 04:30:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3377 boxname=wulflinc2 idbench=1033 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9b64c494b06e0d267a16a958bcbc40bb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb IDLAUNCH: 3377 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 912608 kB Buffers: 13468 kB Cached: 83992 kB SwapCached: 1004 kB Active: 16676 kB Inactive: 83424 kB HighTotal: 131008 kB HighFree: 45528 kB LowTotal: 903652 kB LowFree: 867080 kB SwapTotal: 2097136 kB SwapFree: 2095552 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5600 kB Slab: 16408 kB Committed_AS: 72456 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:34:13 (client local time) WITH STATUS 30 IN 206.622 SECONDS stats: 3377 0 206.622 30
c Parsing PB file... c PARSE ERROR! [line 235] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 209 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ### c -- Clauses(.)/Splits(s): ......................... c ---[ 182]---> BDD-cost: 230 c ---[ 181]---> BDD-cost: 519 c ---[ 180]---> BDD-cost: 230 c ---[ 179]---> BDD-cost: 519 c ---[ 177]---> BDD-cost: 49 c ---[ 176]---> BDD-cost: 43 c ---[ 175]---> BDD-cost: 43 c ---[ 174]---> BDD-cost: 43 c ---[ 173]---> BDD-cost: 43 c ---[ 172]---> BDD-cost: 6 c ---[ 171]---> BDD-cost: 43 c ---[ 169]---> BDD-cost: 2 c ---[ 167]---> BDD-cost: 2 c ---[ 165]---> BDD-cost: 2 c ---[ 163]---> BDD-cost: 2 c ---[ 160]---> BDD-cost: 2 c ---[ 159]---> BDD-cost: 169 c ---[ 158]---> BDD-cost: 272 c ---[ 157]---> BDD-cost: 169 c ---[ 156]---> BDD-cost: 272 c ---[ 155]---> BDD-cost: 169 c ---[ 154]---> BDD-cost: 272 c ---[ 153]---> BDD-cost: 169 c ---[ 152]---> BDD-cost: 272 c ---[ 151]---> BDD-cost: 169 c ---[ 150]---> BDD-cost: 6 c ---[ 149]---> BDD-cost: 272 c ---[ 148]---> BDD-cost: 249 c ---[ 147]---> BDD-cost: 241 c ---[ 146]---> BDD-cost: 249 c ---[ 145]---> BDD-cost: 241 c ---[ 144]---> BDD-cost: 249 c ---[ 143]---> BDD-cost: 241 c ---[ 142]---> BDD-cost: 249 c ---[ 141]---> BDD-cost: 241 c ---[ 140]---> BDD-cost: 249 c ---[ 138]---> BDD-cost: 241 c ---[ 137]---> BDD-cost: 19 c ---[ 136]---> BDD-cost: 24 c ---[ 135]---> BDD-cost: 24 c ---[ 134]---> BDD-cost: 24 c ---[ 133]---> BDD-cost: 24 c ---[ 132]---> BDD-cost: 24 c ---[ 129]---> BDD-cost: 12 c ---[ 127]---> BDD-cost: 6 c ---[ 125]---> BDD-cost: 12 c ---[ 123]---> BDD-cost: 9 c ---[ 121]---> BDD-cost: 4 c ---[ 119]---> BDD-cost: 13 c ---[ 118]---> BDD-cost: 249 c ---[ 117]---> BDD-cost: 102 c ---[ 116]---> BDD-cost: 249 c ---[ 114]---> BDD-cost: 102 c ---[ 113]---> BDD-cost: 249 c ---[ 112]---> BDD-cost: 102 c ---[ 111]---> BDD-cost: 249 c ---[ 110]---> BDD-cost: 102 c ---[ 109]---> BDD-cost: 249 c ---[ 108]---> BDD-cost: 102 c ---[ 107]---> BDD-cost: 7 c ---[ 106]---> BDD-cost: 42 c ---[ 105]---> BDD-cost: 42 c ---[ 104]---> BDD-cost: 3 c ---[ 103]---> BDD-cost: 42 c ---[ 102]---> BDD-cost: 42 c ---[ 101]---> BDD-cost: 40 c ---[ 99]---> BDD-cost: 2 c ---[ 97]---> BDD-cost: 2 c ---[ 95]---> BDD-cost: 2 c ---[ 93]---> BDD-cost: 592 c ---[ 92]---> BDD-cost: 2 c ---[ 90]---> BDD-cost: 2 c ---[ 89]---> BDD-cost: 19 c ---[ 88]---> BDD-cost: 493 c ---[ 87]---> Adder-cost: 112 maxlim: 93 bits: 8/7 c ---[ 86]---> BDD-cost: 592 c ---[ 85]---> BDD-cost: 493 c ---[ 84]---> BDD-cost: 592 c ---[ 83]---> BDD-cost: 493 c ---[ 82]---> BDD-cost: 592 c ---[ 81]---> BDD-cost: 493 c ---[ 80]---> BDD-cost: 592 c ---[ 79]---> BDD-cost: 308 c ---[ 78]---> BDD-cost: 322 c ---[ 77]---> BDD-cost: 521 c ---[ 76]---> BDD-cost: 80 c ---[ 75]---> BDD-cost: 322 c ---[ 74]---> BDD-cost: 521 c ---[ 73]---> BDD-cost: 322 c ---[ 72]---> BDD-cost: 521 c ---[ 71]---> BDD-cost: 322 c ---[ 70]---> BDD-cost: 521 c ---[ 69]---> BDD-cost: 322 c ---[ 68]---> BDD-cost: 314 c ---[ 67]---> BDD-cost: 123 c ---[ 66]---> BDD-cost: 526 c ---[ 65]---> BDD-cost: 80 c ---[ 64]---> BDD-cost: 123 c ---[ 63]---> BDD-cost: 526 c ---[ 62]---> BDD-cost: 123 c ---[ 61]---> BDD-cost: 526 c ---[ 60]---> BDD-cost: 123 c ---[ 59]---> BDD-cost: 526 c ---[ 58]---> BDD-cost: 123 c ---[ 57]---> BDD-cost: 352 c ---[ 56]---> BDD-cost: 249 c ---[ 55]---> BDD-cost: 487 c ---[ 54]---> BDD-cost: 80 c ---[ 53]---> BDD-cost: 249 c ---[ 52]---> BDD-cost: 487 c ---[ 51]---> BDD-cost: 249 c ---[ 50]---> BDD-cost: 487 c ---[ 49]---> BDD-cost: 249 c ---[ 48]---> BDD-cost: 487 c ---[ 47]---> BDD-cost: 249 c ---[ 46]---> BDD-cost: 313 c ---[ 45]---> Sorter-cost: 147 Base: 2 2 2 c ---[ 44]---> BDD-cost: 75 c ---[ 43]---> BDD-cost: 80 c ---[ 42]---> BDD-cost: 75 c ---[ 41]---> BDD-cost: 75 c ---[ 40]---> BDD-cost: 75 c ---[ 39]---> BDD-cost: 63 c ---[ 37]---> BDD-cost: 5 c ---[ 35]---> BDD-cost: 5 c ---[ 33]---> BDD-cost: 5 c ---[ 32]---> BDD-cost: 62 c ---[ 30]---> BDD-cost: 5 c ---[ 28]---> BDD-cost: 4 c ---[ 27]---> BDD-cost: 272 c ---[ 26]---> BDD-cost: 516 c ---[ 25]---> BDD-cost: 272 c ---[ 24]---> BDD-cost: 516 c ---[ 23]---> BDD-cost: 272 c ---[ 22]---> BDD-cost: 516 c ---[ 20]---> BDD-cost: 272 c ---[ 19]---> BDD-cost: 516 c ---[ 18]---> BDD-cost: 272 c ---[ 17]---> BDD-cost: 516 c ---[ 16]---> BDD-cost: 131 c ---[ 15]---> BDD-cost: 561 c ---[ 14]---> BDD-cost: 131 c ---[ 13]---> BDD-cost: 561 c ---[ 12]---> BDD-cost: 131 c ---[ 11]---> BDD-cost: 561 c ---[ 10]---> BDD-cost: 6 c ---[ 9]---> BDD-cost: 131 c ---[ 8]---> BDD-cost: 561 c ---[ 7]---> BDD-cost: 131 c ---[ 6]---> BDD-cost: 561 c ---[ 5]---> BDD-cost: 230 c ---[ 4]---> BDD-cost: 519 c ---[ 3]---> BDD-cost: 230 c ---[ 2]---> BDD-cost: 519 c ---[ 1]---> BDD-cost: 230 c ---[ 0]---> BDD-cost: 519 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 73032 204316 | 24344 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -24[0m c ---[ 0]---> Sorter-cost: 1129 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 75237 209454 | 25079 23 119 5.2 | 0.000 % | c ============================================================================== c [1mFound solution: -33[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 62 | 75247 209511 | 25082 59 330 5.6 | 0.000 % | c | 162 | 75247 209511 | 27590 159 2011 12.6 | 6.760 % | c ============================================================================== c [1mFound solution: -36[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 220 | 75230 209483 | 25076 216 2407 11.1 | 6.760 % | c ============================================================================== c [1mFound solution: -37[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 228 | 75234 209496 | 25078 224 2460 11.0 | 6.760 % | c | 331 | 75234 209496 | 27585 327 5604 17.1 | 6.797 % | c | 481 | 75205 209432 | 30344 476 7867 16.5 | 6.822 % | c | 708 | 75205 209432 | 33378 703 10221 14.5 | 6.821 % | c | 1046 | 74969 208902 | 36716 1031 14493 14.1 | 7.062 % | c ============================================================================== c [1mFound solution: -38[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1203 | 74974 208922 | 24991 1188 18484 15.6 | 7.062 % | c | 1305 | 74862 208667 | 27490 1281 19942 15.6 | 7.185 % | c | 1455 | 74862 208667 | 30239 1431 23275 16.3 | 7.185 % | c | 1680 | 74862 208667 | 33263 1656 26676 16.1 | 7.185 % | c | 2017 | 74862 208667 | 36589 1993 31973 16.0 | 7.185 % | c ============================================================================== c [1mFound solution: -39[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2308 | 74866 208679 | 24955 2284 41532 18.2 | 7.185 % | c | 2409 | 74866 208679 | 27450 2385 42739 17.9 | 7.188 % | c | 2560 | 74866 208679 | 30195 2536 45714 18.0 | 7.188 % | c | 2786 | 74837 208614 | 33215 2759 51484 18.7 | 7.215 % | c | 3123 | 74837 208614 | 36536 3096 58481 18.9 | 7.215 % | c | 3632 | 74798 208528 | 40190 3600 65084 18.1 | 7.271 % | c | 4392 | 74798 208528 | 44209 4360 81658 18.7 | 7.271 % | c | 5534 | 74798 208528 | 48630 5502 103793 18.9 | 7.271 % | c | 7244 | 74798 208528 | 53493 7212 135581 18.8 | 7.271 % | c | 9808 | 74755 208429 | 58842 9771 178768 18.3 | 7.311 % | c | 13653 | 74755 208429 | 64726 13616 276866 20.3 | 7.311 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13994 | 74758 208436 | 24919 13957 282781 20.3 | 7.311 % | c | 14094 | 74758 208436 | 27410 14057 285208 20.3 | 7.314 % | c | 14244 | 74758 208436 | 30151 14207 288086 20.3 | 7.314 % | c | 14469 | 74758 208436 | 33167 14432 292689 20.3 | 7.314 % | c | 14808 | 74758 208436 | 36483 14771 300172 20.3 | 7.314 % | c | 15314 | 74758 208436 | 40132 15277 311034 20.4 | 7.314 % | c | 16074 | 74758 208436 | 44145 16037 327414 20.4 | 7.314 % | c | 17213 | 74758 208436 | 48560 17176 350631 20.4 | 7.314 % | c | 18921 | 74758 208436 | 53416 18884 386547 20.5 | 7.314 % | c | 21488 | 74758 208436 | 58757 21451 436479 20.3 | 7.314 % | c | 25332 | 74758 208436 | 64633 25295 524602 20.7 | 7.314 % | c | 31099 | 74758 208436 | 71096 31062 652469 21.0 | 7.314 % | c | 39748 | 74718 208346 | 78206 39699 855543 21.6 | 7.357 % | c ============================================================================== c [1mFound solution: -41[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45406 | 74721 208353 | 24907 45357 989059 21.8 | 7.357 % | c | 45506 | 74721 208353 | 27397 15173 320832 21.1 | 7.360 % | c | 45657 | 74721 208353 | 30137 15324 323126 21.1 | 7.360 % | c | 45882 | 74721 208353 | 33151 15549 327530 21.1 | 7.360 % | c | 46219 | 74721 208353 | 36466 15886 334077 21.0 | 7.360 % | c | 46725 | 74721 208353 | 40112 16392 342815 20.9 | 7.360 % | c | 47484 | 74721 208353 | 44124 17151 357204 20.8 | 7.360 % | c | 48623 | 74721 208353 | 48536 18290 384674 21.0 | 7.360 % | c | 50331 | 74721 208353 | 53390 19998 414575 20.7 | 7.360 % | c | 52894 | 74721 208353 | 58729 22561 462369 20.5 | 7.360 % | c | 56738 | 74721 208353 | 64602 26405 535134 20.3 | 7.360 % | c | 62504 | 74684 208249 | 71062 8011 142662 17.8 | 7.372 % | c | 71155 | 74527 207847 | 78168 11113 215104 19.4 | 7.548 % | c ============================================================================== c [1mOptimal solution: -41[0m s OPTIMUM FOUND v X11_bit0 X11_bit1 X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X11_bit13 -X11_bit14 -X11_bit15 -X11_bit16 -X12_bit0 X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X12_bit13 -X12_bit14 -X12_bit15 -X12_bit16 X13_bit0 -X13_bit1 -X13_bit2 X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X13_bit13 -X13_bit14 -X13_bit15 -X13_bit16 X14_bit0 -X14_bit1 -X14_bit2 X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X14_bit13 -X14_bit14 -X14_bit15 -X14_bit16 X15_bit0 X15_bit1 X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X15_bit13 -X15_bit14 -X15_bit15 -X15_bit16 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X21_bit13 -X21_bit14 -X21_bit15 -X21_bit16 X22_bit0 -X22_bit1 X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X22_bit13 -X22_bit14 -X22_bit15 -X22_bit16 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X23_bit13 -X23_bit14 -X23_bit15 -X23_bit16 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X24_bit13 -X24_bit14 -X24_bit15 -X24_bit16 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X25_bit13 -X25_bit14 -X25_bit15 -X25_bit16 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X31_bit13 -X31_bit14 -X31_bit15 -X31_bit16 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X32_bit13 -X32_bit14 -X32_bit15 -X32_bit16 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X33_bit13 -X33_bit14 -X33_bit15 -X33_bit16 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X34_bit13 -X34_bit14 -X34_bit15 -X34_bit16 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X35_bit13 -X35_bit14 -X35_bit15 -X35_bit16 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X41_bit13 -X41_bit14 -X41_bit15 -X41_bit16 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X42_bit13 -X42_bit14 -X42_bit15 -X42_bit16 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X43_bit13 -X43_bit14 -X43_bit15 -X43_bit16 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X44_bit13 -X44_bit14 -X44_bit15 -X44_bit16 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X45_bit13 -X45_bit14 -X45_bit15 -X45_bit16 -X51_bit0 X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X51_bit13 -X51_bit14 -X51_bit15 -X51_bit16 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X52_bit13 -X52_bit14 -X52_bit15 -X52_bit16 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X53_bit13 -X53_bit14 -X53_bit15 -X53_bit16 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X54_bit13 -X54_bit14 -X54_bit15 -X54_bit16 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X55_bit13 -X55_bit14 -X55_bit15 -X55_bit16 -T121_bit0 T122_bit0 -T123_bit0 -T124_bit0 -T125_bit0 -T131_bit0 -T132_bit0 -T133_bit0 -T134_bit0 -T135_bit0 -T141_bit0 -T142_bit0 -T143_bit0 -T144_bit0 -T145_bit0 T151_bit0 -T152_bit0 -T153_bit0 -T154_bit0 -T155_bit0 -T231_bit0 -T232_bit0 T233_bit0 T234_bit0 -T235_bit0 -T241_bit0 -T242_bit0 -T243_bit0 T244_bit0 T245_bit0 T251_bit0 -T252_bit0 -T253_bit0 -T254_bit0 T255_bit0 T341_bit0 T342_bit0 -T343_bit0 -T344_bit0 -T345_bit0 T351_bit0 -T352_bit0 -T353_bit0 T354_bit0 -T355_bit0 T451_bit0 T452_bit0 -T453_bit0 T454_bit0 T455_bit0 W11_bit0 W12_bit0 W13_bit0 W14_bit0 W15_bit0 -W21_bit0 W22_bit0 -W23_bit0 -W24_bit0 -W25_bit0 -W31_bit0 -W32_bit0 -W33_bit0 -W34_bit0 -W35_bit0 -W41_bit0 -W42_bit0 -W43_bit0 -W44_bit0 -W45_bit0 W51_bit0 -W52_bit0 -W53_bit0 -W54_bit0 -W55_bit0 -S24_bit_7 -S24_bit_6 -S24_bit_5 -S24_bit_4 -S24_bit_3 -S24_bit_2 -S24_bit_1 -S24_bit0 -S24_bit1 -S24_bit2 -S24_bit3 -S24_bit4 -S24_bit5 -S24_bit6 -S24_bit7 -S24_bit8 -S24_bit9 -S24_bit10 -S24_bit11 -S24_bit12 -S54_bit_7 -S54_bit_6 -S54_bit_5 -S54_bit_4 -S54_bit_3 -S54_bit_2 -S54_bit_1 -S54_bit0 -S54_bit1 -S54_bit2 -S54_bit3 -S54_bit4 -S54_bit5 -S54_bit6 -S54_bit7 -S54_bit8 -S54_bit9 -S54_bit10 -S54_bit11 -S54_bit12 -S25_bit_7 -S25_bit_6 -S25_bit_5 -S25_bit_4 -S25_bit_3 -S25_bit_2 -S25_bit_1 -S25_bit0 -S25_bit1 -S25_bit2 -S25_bit3 -S25_bit4 -S25_bit5 -S25_bit6 -S25_bit7 -S25_bit8 -S25_bit9 -S25_bit10 -S25_bit11 -S25_bit12 -S55_bit_7 -S55_bit_6 -S55_bit_5 -S55_bit_4 -S55_bit_3 -S55_bit_2 -S55_bit_1 -S55_bit0 -S55_bit1 -S55_bit2 -S55_bit3 -S55_bit4 -S55_bit5 -S55_bit6 -S55_bit7 -S55_bit8 -S55_bit9 -S55_bit10 -S55_bit11 -S55_bit12 -S31_bit_7 -S31_bit_6 -S31_bit_5 -S31_bit_4 -S31_bit_3 -S31_bit_2 -S31_bit_1 -S31_bit0 -S31_bit1 -S31_bit2 -S31_bit3 -S31_bit4 -S31_bit5 -S31_bit6 -S31_bit7 -S31_bit8 -S31_bit9 -S31_bit10 -S31_bit11 -S31_bit12 -S32_bit_7 -S32_bit_6 -S32_bit_5 -S32_bit_4 -S32_bit_3 -S32_bit_2 -S32_bit_1 -S32_bit0 -S32_bit1 -S32_bit2 -S32_bit3 -S32_bit4 -S32_bit5 -S32_bit6 -S32_bit7 -S32_bit8 -S32_bit9 -S32_bit10 -S32_bit11 -S32_bit12 -S33_bit_7 -S33_bit_6 -S33_bit_5 -S33_bit_4 -S33_bit_3 -S33_bit_2 -S33_bit_1 -S33_bit0 -S33_bit1 -S33_bit2 -S33_bit3 -S33_bit4 -S33_bit5 -S33_bit6 -S33_bit7 -S33_bit8 -S33_bit9 -S33_bit10 -S33_bit11 -S33_bit12 -S34_bit_7 -S34_bit_6 -S34_bit_5 -S34_bit_4 -S34_bit_3 -S34_bit_2 -S34_bit_1 -S34_bit0 -S34_bit1 -S34_bit2 -S34_bit3 -S34_bit4 -S34_bit5 -S34_bit6 -S34_bit7 -S34_bit8 -S34_bit9 -S34_bit10 -S34_bit11 -S34_bit12 -S35_bit_7 -S35_bit_6 -S35_bit_5 -S35_bit_4 -S35_bit_3 -S35_bit_2 -S35_bit_1 -S35_bit0 -S35_bit1 -S35_bit2 -S35_bit3 -S35_bit4 -S35_bit5 -S35_bit6 -S35_bit7 -S35_bit8 -S35_bit9 -S35_bit10 -S35_bit11 -S35_bit12 -S41_bit_7 -S41_bit_6 -S41_bit_5 -S41_bit_4 -S41_bit_3 -S41_bit_2 -S41_bit_1 -S41_bit0 -S41_bit1 -S41_bit2 -S41_bit3 -S41_bit4 -S41_bit5 -S41_bit6 -S41_bit7 -S41_bit8 -S41_bit9 -S41_bit10 -S41_bit11 -S41_bit12 -S42_bit_7 -S42_bit_6 -S42_bit_5 -S42_bit_4 -S42_bit_3 -S42_bit_2 -S42_bit_1 -S42_bit0 -S42_bit1 -S42_bit2 -S42_bit3 -S42_bit4 -S42_bit5 -S42_bit6 -S42_bit7 -S42_bit8 -S42_bit9 -S42_bit10 -S42_bit11 -S42_bit12 -S43_bit_7 -S43_bit_6 -S43_bit_5 -S43_bit_4 -S43_bit_3 -S43_bit_2 -S43_bit_1 -S43_bit0 -S43_bit1 -S43_bit2 -S43_bit3 -S43_bit4 -S43_bit5 -S43_bit6 -S43_bit7 -S43_bit8 -S43_bit9 -S43_bit10 -S43_bit11 -S43_bit12 -S44_bit_7 -S44_bit_6 -S44_bit_5 -S44_bit_4 -S44_bit_3 -S44_bit_2 -S44_bit_1 -S44_bit0 -S44_bit1 -S44_bit2 -S44_bit3 -S44_bit4 -S44_bit5 -S44_bit6 -S44_bit7 -S44_bit8 -S44_bit9 -S44_bit10 -S44_bit11 -S44_bit12 -S45_bit_7 -S45_bit_6 -S45_bit_5 -S45_bit_4 -S45_bit_3 -S45_bit_2 -S45_bit_1 -S45_bit0 -S45_bit1 -S45_bit2 -S45_bit3 -S45_bit4 -S45_bit5 -S45_bit6 -S45_bit7 -S45_bit8 -S45_bit9 -S45_bit10 -S45_bit11 -S45_bit12 -S51_bit_7 -S51_bit_6 S51_bit_5 -S51_bit_4 S51_bit_3 -S51_bit_2 -S51_bit_1 S51_bit0 S51_bit1 S51_bit2 S51_bit3 -S51_bit4 -S51_bit5 -S51_bit6 -S51_bit7 -S51_bit8 -S51_bit9 -S51_bit10 -S51_bit11 -S51_bit12 -S52_bit_7 -S52_bit_6 -S52_bit_5 -S52_bit_4 -S52_bit_3 -S52_bit_2 -S52_bit_1 -S52_bit0 -S52_bit1 -S52_bit2 -S52_bit3 -S52_bit4 -S52_bit5 -S52_bit6 -S52_bit7 -S52_bit8 -S52_bit9 -S52_bit10 -S52_bit11 -S52_bit12 -S53_bit_7 -S53_bit_6 -S53_bit_5 -S53_bit_4 -S53_bit_3 -S53_bit_2 -S53_bit_1 -S53_bit0 -S53_bit1 -S53_bit2 -S53_bit3 -S53_bit4 -S53_bit5 -S53_bit6 -S53_bit7 -S53_bit8 -S53_bit9 -S53_bit10 -S53_bit11 -S53_bit12 -V148_bit_7 -V148_bit_6 -V148_bit_5 -V148_bit_4 -V148_bit_3 -V148_bit_2 -V148_bit_1 -V148_bit0 -V148_bit1 -V148_bit2 -V148_bit3 -V148_bit4 -V148_bit5 -V148_bit6 -V148_bit7 -V148_bit8 -V148_bit9 -V148_bit10 -V148_bit11 -V148_bit12 -V150_bit_7 -V150_bit_6 -V150_bit_5 -V150_bit_4 -V150_bit_3 -V150_bit_2 -V150_bit_1 -V150_bit0 -V150_bit1 -V150_bit2 -V150_bit3 -V150_bit4 -V150_bit5 -V150_bit6 -V150_bit7 -V150_bit8 -V150_bit9 -V150_bit10 -V150_bit11 -V150_bit12 -Q246_bit_7 -Q246_bit_6 -Q246_bit_5 -Q246_bit_4 -Q246_bit_3 -Q246_bit_2 -Q246_bit_1 -Q246_bit0 -Q246_bit1 -Q246_bit2 -Q246_bit3 -Q246_bit4 -Q246_bit5 -Q246_bit6 -Q246_bit7 -Q246_bit8 -Q246_bit9 -Q246_bit10 -Q246_bit11 -Q246_bit12 -S11_bit_7 S11_bit_6 -S11_bit_5 S11_bit_4 S11_bit_3 -S11_bit_2 -S11_bit_1 -S11_bit0 -S11_bit1 -S11_bit2 -S11_bit3 -S11_bit4 -S11_bit5 -S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -S21_bit_7 -S21_bit_6 -S21_bit_5 -S21_bit_4 -S21_bit_3 -S21_bit_2 -S21_bit_1 -S21_bit0 -S21_bit1 -S21_bit2 -S21_bit3 -S21_bit4 -S21_bit5 -S21_bit6 -S21_bit7 -S21_bit8 -S21_bit9 -S21_bit10 -S21_bit11 -S21_bit12 S12_bit_7 -S12_bit_6 -S12_bit_5 S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 -S12_bit0 -S12_bit1 -S12_bit2 -S12_bit3 -S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 S22_bit_7 S22_bit_6 -S22_bit_5 -S22_bit_4 -S22_bit_3 -S22_bit_2 -S22_bit_1 S22_bit0 -S22_bit1 S22_bit2 -S22_bit3 -S22_bit4 -S22_bit5 -S22_bit6 -S22_bit7 -S22_bit8 -S22_bit9 -S22_bit10 -S22_bit11 -S22_bit12 -S13_bit_7 -S13_bit_6 S13_bit_5 -S13_bit_4 -S13_bit_3 S13_bit_2 -S13_bit_1 -S13_bit0 -S13_bit1 -S13_bit2 -S13_bit3 -S13_bit4 -S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -S23_bit_7 -S23_bit_6 -S23_bit_5 -S23_bit_4 -S23_bit_3 -S23_bit_2 -S23_bit_1 -S23_bit0 -S23_bit1 -S23_bit2 -S23_bit3 -S23_bit4 -S23_bit5 -S23_bit6 -S23_bit7 -S23_bit8 -S23_bit9 -S23_bit10 -S23_bit11 -S23_bit12 -S14_bit_7 -S14_bit_6 -S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 S14_bit0 -S14_bit1 -S14_bit2 -S14_bit3 -S14_bit4 -S14_bit5 -S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 S15_bit_7 -S15_bit_6 S15_bit_5 -S15_bit_4 -S15_bit_3 S15_bit_2 S15_bit_1 -S15_bit0 -S15_bit1 -S15_bit2 -S15_bit3 -S15_bit4 -S15_bit5 -S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 c _______________________________________________________________________________ c c restarts : 52 c conflicts : 72614 (352 /sec) c decisions : 198116 (960 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 206.331 s c _______________________________________________________________________________
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/8400/stat): 8400 (minisat+_script) R 8399 8400 6872 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797456774 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8400/statm): 174 3 169 147 0 27 0 [pid=8400] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=8401 New process pid=8402 New process pid=8403 execve syscall for /bin/sed executable One traced child (pid=8402) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=8403) exited with status: 0 One traced child (pid=8401) exited with status: 0 New process pid=8404 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb One traced child (pid=8404) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=8405 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3048 0 0 0 969 11 0 0 25 0 1 0 1797456781 13303808 2913 4294967295 134512640 135167914 3221224448 3221223120 134562239 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8405/statm): 3248 2913 162 162 0 3086 0 [pid=8405] vsize: 12992 Current children cumulated CPU time (s) 9.82 Current children cumulated vsize (Kb) 15120 [startup+20.004 s] Raw data (loadavg): 0.94 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3187 0 0 0 1965 13 0 0 25 0 1 0 1797456781 13897728 3052 4294967295 134512640 135167914 3221224448 3221223152 134562535 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 3393 3052 162 162 0 3231 0 [pid=8405] vsize: 13572 Current children cumulated CPU time (s) 19.8 Current children cumulated vsize (Kb) 15700 [startup+30.0057 s] Raw data (loadavg): 0.95 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3344 0 0 0 2960 14 0 0 25 0 1 0 1797456781 14520320 3209 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 3545 3209 162 162 0 3383 0 [pid=8405] vsize: 14180 Current children cumulated CPU time (s) 29.76 Current children cumulated vsize (Kb) 16308 [startup+40.0064 s] Raw data (loadavg): 0.96 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3470 0 0 0 3959 14 0 0 25 0 1 0 1797456781 15101952 3335 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 3687 3335 162 162 0 3525 0 [pid=8405] vsize: 14748 Current children cumulated CPU time (s) 39.75 Current children cumulated vsize (Kb) 16876 [startup+50.0081 s] Raw data (loadavg): 0.96 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3587 0 0 0 4957 15 0 0 25 0 1 0 1797456781 15581184 3452 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 3804 3452 162 162 0 3642 0 [pid=8405] vsize: 15216 Current children cumulated CPU time (s) 49.74 Current children cumulated vsize (Kb) 17344 [startup+60.0088 s] Raw data (loadavg): 0.97 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3707 0 0 0 5955 16 0 0 25 0 1 0 1797456781 16064512 3572 4294967295 134512640 135167914 3221224448 3221223120 134562221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 3922 3572 162 162 0 3760 0 [pid=8405] vsize: 15688 Current children cumulated CPU time (s) 59.73 Current children cumulated vsize (Kb) 17816 [startup+70.0095 s] Raw data (loadavg): 0.97 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3824 0 0 0 6953 17 0 0 25 0 1 0 1797456781 16535552 3689 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4037 3689 162 162 0 3875 0 [pid=8405] vsize: 16148 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 18276 [startup+80.0112 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3937 0 0 0 7953 18 0 0 25 0 1 0 1797456781 16990208 3802 4294967295 134512640 135167914 3221224448 3221223152 134562502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4148 3802 162 162 0 3986 0 [pid=8405] vsize: 16592 Current children cumulated CPU time (s) 79.73 Current children cumulated vsize (Kb) 18720 [startup+90.0119 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4036 0 0 0 8952 18 0 0 25 0 1 0 1797456781 17518592 3901 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4277 3901 162 162 0 4115 0 [pid=8405] vsize: 17108 Current children cumulated CPU time (s) 89.72 Current children cumulated vsize (Kb) 19236 [startup+100.013 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4125 0 0 0 9951 19 0 0 25 0 1 0 1797456781 17899520 3990 4294967295 134512640 135167914 3221224448 3221223152 134562869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4370 3990 162 162 0 4208 0 [pid=8405] vsize: 17480 Current children cumulated CPU time (s) 99.72 Current children cumulated vsize (Kb) 19608 [startup+110.013 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4227 0 0 0 10949 20 0 0 25 0 1 0 1797456781 18333696 4092 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4476 4092 162 162 0 4314 0 [pid=8405] vsize: 17904 Current children cumulated CPU time (s) 109.71 Current children cumulated vsize (Kb) 20032 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4312 0 0 0 11947 21 0 0 25 0 1 0 1797456781 18665472 4177 4294967295 134512640 135167914 3221224448 3221223088 134562079 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4557 4177 162 162 0 4395 0 [pid=8405] vsize: 18228 Current children cumulated CPU time (s) 119.7 Current children cumulated vsize (Kb) 20356 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4382 0 0 0 12947 21 0 0 25 0 1 0 1797456781 18960384 4247 4294967295 134512640 135167914 3221224448 3221223152 134562874 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4247 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 129.7 Current children cumulated vsize (Kb) 20644 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4383 0 0 0 13947 21 0 0 25 0 1 0 1797456781 18960384 4248 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4248 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 139.7 Current children cumulated vsize (Kb) 20644 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 14947 21 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 149.7 Current children cumulated vsize (Kb) 20644 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 15948 21 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 159.71 Current children cumulated vsize (Kb) 20644 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 16948 21 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 169.71 Current children cumulated vsize (Kb) 20644 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 17948 22 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223136 134556119 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 179.72 Current children cumulated vsize (Kb) 20644 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 18948 22 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 189.72 Current children cumulated vsize (Kb) 20644 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 8405 Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8400/statm): 532 234 485 147 0 385 0 [pid=8400] vsize: 2128 Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 19949 22 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562535 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0 [pid=8405] vsize: 18516 Current children cumulated CPU time (s) 199.73 Current children cumulated vsize (Kb) 20644 One traced child (pid=8405) exited with status: 30 One traced child (pid=8400) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 206.891 CPU time (s): 206.622 CPU user time (s): 206.36 CPU system time (s): 0.26196 CPU usage (%): 99.8699 Max. virtual memory (cumulated for all children) (Kb): 20644
Verifier: OK -41