Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32c2.opb |
MD5SUM | b78d16df5ec546c41fce5f9f07c0fd92 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 207 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 498 |
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 | 498 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 498 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.03184 |
Number of variables | 498 |
Total number of constraints | 2431 |
Number of constraints which are clauses | 2431 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 32 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc10 THE 2005-04-13 20:47:49 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=1364 boxname=wulflinc10 idbench=152 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: b78d16df5ec546c41fce5f9f07c0fd92 /oldhome/oroussel/tmp/wulflinc10/normalized-ii32c2.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc10/normalized-ii32c2.opb IDLAUNCH: 1364 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 2 cpu MHz : 450.999 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: 908772 kB Buffers: 34024 kB Cached: 72368 kB SwapCached: 164 kB Active: 49796 kB Inactive: 59604 kB HighTotal: 131008 kB HighFree: 54908 kB LowTotal: 903652 kB LowFree: 853864 kB SwapTotal: 2097136 kB SwapFree: 2096972 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 10860 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 20:59:12 (client local time) WITH STATUS 30 IN 683.043 SECONDS stats: 1364 0 683.043 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 2431 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 | 2431 12171 | 810 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 229[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:18940 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 25031 65035 | 8343 17 834 49.1 | 0.000 % | c | 117 | 25031 65035 | 9177 117 8434 72.1 | 0.006 % | c | 267 | 25031 65035 | 10095 267 18454 69.1 | 0.006 % | c ============================================================================== c [1mFound solution: 214[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 | 458 | 25073 65214 | 8357 454 27676 61.0 | 0.006 % | c | 559 | 25073 65214 | 9192 555 34028 61.3 | 0.323 % | c | 713 | 25032 65131 | 10111 707 44845 63.4 | 0.459 % | c | 939 | 25032 65131 | 11123 933 57611 61.7 | 0.459 % | c | 1277 | 25032 65131 | 12235 1271 80019 63.0 | 0.459 % | c | 1783 | 25006 65077 | 13459 1776 114214 64.3 | 0.549 % | c ============================================================================== c [1mFound solution: 210[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 | 1804 | 25016 65123 | 8338 1797 115471 64.3 | 0.549 % | c | 1906 | 25016 65123 | 9171 1899 126277 66.5 | 0.722 % | c | 2056 | 25016 65123 | 10088 2049 134544 65.7 | 0.722 % | c | 2285 | 25016 65123 | 11097 2278 152398 66.9 | 0.722 % | c | 2623 | 24967 65022 | 12207 2614 179756 68.8 | 0.890 % | c | 3130 | 24657 64370 | 13428 3112 223186 71.7 | 1.993 % | c | 3889 | 24657 64370 | 14771 3871 282163 72.9 | 1.993 % | c | 5029 | 24590 64225 | 16248 5008 397301 79.3 | 2.245 % | c | 6738 | 24489 64002 | 17873 6714 560641 83.5 | 2.638 % | c | 9300 | 24417 63848 | 19660 9274 816084 88.0 | 2.903 % | c | 13148 | 24296 63589 | 21626 13119 1093845 83.4 | 3.348 % | c | 18916 | 24143 63258 | 23789 18882 1567412 83.0 | 3.922 % | c | 27565 | 23741 62382 | 26168 14386 1059651 73.7 | 5.451 % | c | 40539 | 23625 62128 | 28785 13813 922054 66.8 | 5.896 % | c ============================================================================== c [1mFound solution: 209[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 | 50260 | 23564 62014 | 7854 23532 1691813 71.9 | 5.896 % | c | 50362 | 22983 60737 | 8639 5972 363407 60.9 | 8.461 % | c | 50514 | 22983 60737 | 9503 6124 379534 62.0 | 8.461 % | c | 50741 | 22870 60486 | 10453 6274 388103 61.9 | 8.905 % | c | 51079 | 22870 60486 | 11499 6612 406645 61.5 | 8.905 % | c | 51586 | 22870 60486 | 12648 7119 431847 60.7 | 8.905 % | c | 52345 | 22870 60486 | 13913 7878 471382 59.8 | 8.905 % | c | 53484 | 22574 59836 | 15305 9011 545279 60.5 | 10.046 % | c | 55192 | 22574 59836 | 16835 10719 683619 63.8 | 10.046 % | c | 57754 | 22371 59385 | 18519 13273 900059 67.8 | 10.845 % | c | 61600 | 22322 59276 | 20371 17118 1191328 69.6 | 11.038 % | c | 67366 | 22278 59180 | 22408 22883 1650338 72.1 | 11.206 % | c ============================================================================== c [1mFound solution: 208[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 | 73476 | 22218 59037 | 7406 16343 1067329 65.3 | 11.206 % | c | 73576 | 22218 59037 | 8146 8272 481817 58.2 | 11.468 % | c | 73726 | 22168 58929 | 8961 8421 493849 58.6 | 11.655 % | c | 73951 | 22168 58929 | 9857 8646 507292 58.7 | 11.655 % | c | 74291 | 22125 58832 | 10843 8985 540245 60.1 | 11.829 % | c | 74798 | 22025 58614 | 11927 9490 565624 59.6 | 12.209 % | c | 75557 | 22025 58614 | 13120 10249 624092 60.9 | 12.209 % | c | 76696 | 22025 58614 | 14432 11388 700164 61.5 | 12.209 % | c | 78404 | 22025 58614 | 15875 13096 796105 60.8 | 12.209 % | c ============================================================================== c [1mFound solution: 207[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 | 80820 | 22051 58691 | 7350 15512 938795 60.5 | 12.209 % | c | 80920 | 22051 58691 | 8085 7856 354692 45.1 | 12.202 % | c | 81070 | 22051 58691 | 8893 8006 361980 45.2 | 12.202 % | c | 81298 | 22051 58691 | 9782 8234 373402 45.3 | 12.202 % | c | 81635 | 22051 58691 | 10761 8571 391418 45.7 | 12.202 % | c | 82143 | 22051 58691 | 11837 9079 433890 47.8 | 12.202 % | c | 82902 | 22051 58691 | 13020 9838 474297 48.2 | 12.202 % | c | 84045 | 22051 58691 | 14323 10981 546772 49.8 | 12.202 % | c | 85755 | 22051 58691 | 15755 12691 649979 51.2 | 12.202 % | c | 88317 | 21968 58502 | 17330 15251 791410 51.9 | 12.543 % | c | 92161 | 21840 58212 | 19064 19092 988932 51.8 | 13.064 % | c | 97927 | 21840 58212 | 20970 13948 670487 48.1 | 13.064 % | c | 106578 | 21651 57795 | 23067 22589 1336693 59.2 | 13.798 % | c | 119552 | 21361 57145 | 25374 22451 1254969 55.9 | 14.949 % | c | 139013 | 21165 56713 | 27911 27846 1363308 49.0 | 15.703 % | c | 168207 | 20231 54645 | 30702 14460 632089 43.7 | 19.165 % | c | 211996 | 20231 54645 | 33773 21920 1245975 56.8 | 19.165 % | c ============================================================================== c [1mOptimal solution: 207[0m s OPTIMUM FOUND 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 c _______________________________________________________________________________ c c restarts : 62 c conflicts : 219909 (322 /sec) c decisions : 389823 (571 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 682.853 s c _______________________________________________________________________________ #### 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.86 0.97 0.91 2/54 27791 Raw data (stat): 27791 (runsolver) R 27790 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420733962 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+9.99992 s] Raw data (loadavg): 0.88 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 1962 0 0 0 993 5 0 0 25 0 1 0 420733962 9945088 1936 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2428 1936 603 41 0 2387 0 vsize: 9712 [startup+20.0003 s] Raw data (loadavg): 0.90 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 2462 0 0 0 1991 7 0 0 25 0 1 0 420733962 11956224 2436 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2919 2436 603 41 0 2878 0 vsize: 11676 [startup+30.0005 s] Raw data (loadavg): 0.91 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 2782 0 0 0 2990 8 0 0 25 0 1 0 420733962 13287424 2756 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3244 2756 603 41 0 3203 0 vsize: 12976 [startup+40.0005 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3058 0 0 0 3988 9 0 0 25 0 1 0 420733962 14520320 3032 4294967295 134512640 134672761 3221224640 3221223840 134557913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3545 3032 603 41 0 3504 0 vsize: 14180 [startup+50.001 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3340 0 0 0 4987 10 0 0 25 0 1 0 420733962 15589376 3314 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3806 3314 603 41 0 3765 0 vsize: 15224 [startup+60.0009 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3604 0 0 0 5986 12 0 0 25 0 1 0 420733962 16646144 3578 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4064 3578 603 41 0 4023 0 vsize: 16256 [startup+70.0012 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3874 0 0 0 6985 13 0 0 25 0 1 0 420733962 17715200 3848 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4325 3848 603 41 0 4284 0 vsize: 17300 [startup+80.0007 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3994 0 0 0 7984 13 0 0 25 0 1 0 420733962 18247680 3968 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4455 3968 603 41 0 4414 0 vsize: 17820 [startup+90.0006 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3994 0 0 0 8985 13 0 0 25 0 1 0 420733962 18247680 3968 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4455 3968 603 41 0 4414 0 vsize: 17820 [startup+100.001 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3994 0 0 0 9985 13 0 0 25 0 1 0 420733962 18247680 3968 4294967295 134512640 134672761 3221224640 3221223744 134560134 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4455 3968 603 41 0 4414 0 vsize: 17820 [startup+110 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3994 0 0 0 10985 13 0 0 25 0 1 0 420733962 18247680 3968 4294967295 134512640 134672761 3221224640 3221223744 134559981 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4455 3968 603 41 0 4414 0 vsize: 17820 [startup+120.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 3996 0 0 0 11985 13 0 0 25 0 1 0 420733962 18247680 3970 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4455 3970 603 41 0 4414 0 vsize: 17820 [startup+130.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4004 0 0 0 12985 14 0 0 25 0 1 0 420733962 18247680 3978 4294967295 134512640 134672761 3221224640 3221223744 134559887 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4455 3978 603 41 0 4414 0 vsize: 17820 [startup+140 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4004 0 0 0 13984 14 0 0 25 0 1 0 420733962 18247680 3978 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4455 3978 603 41 0 4414 0 vsize: 17820 [startup+150.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4010 0 0 0 14985 14 0 0 25 0 1 0 420733962 18386944 3984 4294967295 134512640 134672761 3221224640 3221223824 134559345 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3984 603 41 0 4448 0 vsize: 17956 [startup+160 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 15985 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+170 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 16985 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+180 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 17985 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+189.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 18985 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+199.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 19985 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+209.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 20986 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134561133 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+220 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 21986 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+230 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 22986 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+239.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 23986 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+250 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4011 0 0 0 24986 14 0 0 25 0 1 0 420733962 18386944 3985 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3985 603 41 0 4448 0 vsize: 17956 [startup+260 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 25986 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+270.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 26987 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+280 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 27987 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+290 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 28987 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223744 134559991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+299.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 29987 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+309.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 30987 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+320 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 31988 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+330 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 32988 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223744 134560477 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+339.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 33988 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223744 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+349.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 34988 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+360 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 35988 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+370 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 36989 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+380 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4012 0 0 0 37989 14 0 0 25 0 1 0 420733962 18386944 3986 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3986 603 41 0 4448 0 vsize: 17956 [startup+390 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4013 0 0 0 38989 14 0 0 25 0 1 0 420733962 18386944 3987 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3987 603 41 0 4448 0 vsize: 17956 [startup+400 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4018 0 0 0 39989 14 0 0 25 0 1 0 420733962 18386944 3992 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3992 603 41 0 4448 0 vsize: 17956 [startup+410 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4018 0 0 0 40989 14 0 0 25 0 1 0 420733962 18386944 3992 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3992 603 41 0 4448 0 vsize: 17956 [startup+420 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4018 0 0 0 41989 14 0 0 25 0 1 0 420733962 18386944 3992 4294967295 134512640 134672761 3221224640 3221223744 134560367 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3992 603 41 0 4448 0 vsize: 17956 [startup+430.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4018 0 0 0 42990 14 0 0 25 0 1 0 420733962 18386944 3992 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3992 603 41 0 4448 0 vsize: 17956 [startup+440 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4021 0 0 0 43990 14 0 0 25 0 1 0 420733962 18386944 3995 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3995 603 41 0 4448 0 vsize: 17956 [startup+450.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4022 0 0 0 44990 14 0 0 25 0 1 0 420733962 18386944 3996 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 3996 603 41 0 4448 0 vsize: 17956 [startup+460 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 45990 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+470.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 46990 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+480.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 47991 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+490 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 48991 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+500.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 49991 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+510 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 50991 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+520 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 51991 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+530 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 52991 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+540 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 53991 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+550 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4028 0 0 0 54992 14 0 0 25 0 1 0 420733962 18386944 4002 4294967295 134512640 134672761 3221224640 3221223824 134558648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4002 603 41 0 4448 0 vsize: 17956 [startup+560 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4041 0 0 0 55992 15 0 0 25 0 1 0 420733962 18386944 4015 4294967295 134512640 134672761 3221224640 3221223804 134565024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4489 4015 603 41 0 4448 0 vsize: 17956 [startup+570.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4057 0 0 0 56992 15 0 0 25 0 1 0 420733962 18534400 4031 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4525 4031 603 41 0 4484 0 vsize: 18100 [startup+580 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4312 0 0 0 57991 15 0 0 25 0 1 0 420733962 19730432 4286 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4817 4286 603 41 0 4776 0 vsize: 19268 [startup+590 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4533 0 0 0 58991 16 0 0 25 0 1 0 420733962 20525056 4507 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4507 603 41 0 4970 0 vsize: 20044 [startup+600 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4538 0 0 0 59991 16 0 0 25 0 1 0 420733962 20660224 4512 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4512 603 41 0 5003 0 vsize: 20176 [startup+610.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4549 0 0 0 60991 16 0 0 25 0 1 0 420733962 20660224 4523 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4523 603 41 0 5003 0 vsize: 20176 [startup+620.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4550 0 0 0 61991 16 0 0 25 0 1 0 420733962 20660224 4524 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4524 603 41 0 5003 0 vsize: 20176 [startup+630.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4556 0 0 0 62991 16 0 0 25 0 1 0 420733962 20660224 4530 4294967295 134512640 134672761 3221224640 3221223792 134565086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4530 603 41 0 5003 0 vsize: 20176 [startup+640 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4556 0 0 0 63991 16 0 0 25 0 1 0 420733962 20660224 4530 4294967295 134512640 134672761 3221224640 3221223776 134560590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4530 603 41 0 5003 0 vsize: 20176 [startup+650 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4556 0 0 0 64992 16 0 0 25 0 1 0 420733962 20660224 4530 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4530 603 41 0 5003 0 vsize: 20176 [startup+660 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4556 0 0 0 65991 16 0 0 25 0 1 0 420733962 20660224 4530 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4530 603 41 0 5003 0 vsize: 20176 [startup+670 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4564 0 0 0 66991 16 0 0 25 0 1 0 420733962 20660224 4538 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5044 4538 603 41 0 5003 0 vsize: 20176 [startup+680.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4571 0 0 0 67992 16 0 0 25 0 1 0 420733962 20807680 4545 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5080 4545 603 41 0 5039 0 vsize: 20320 [startup+682.955 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 27791 Raw data (stat): 27791 (minisat+) R 27790 25347 25346 0 -1 0 4571 0 0 0 67992 16 0 0 25 0 1 0 420733962 20807680 4545 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5080 4545 603 41 0 5039 0 vsize: 0 Child status: 30 Real time (s): 682.955 CPU time (s): 683.043 CPU user time (s): 682.863 CPU system time (s): 0.179972 CPU usage (%): 100.013 Max. virtual memory (Kb): 20320 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 207 #### END VERIFIER DATA ####