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 wulflinc11 THE 2005-05-25 16:26:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21734 boxname=wulflinc11 idbench=152 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: b78d16df5ec546c41fce5f9f07c0fd92 /oldhome/oroussel/tmp/wulflinc11/normalized-ii32c2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-ii32c2.opb IDLAUNCH: 21734 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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.028 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: 795904 kB Buffers: 33836 kB Cached: 184080 kB SwapCached: 772 kB Active: 74916 kB Inactive: 145100 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 795652 kB SwapTotal: 2097136 kB SwapFree: 2095468 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5028 kB Slab: 13136 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 16:37:54 (client local time) WITH STATUS 30 IN 680.408 SECONDS stats: 21734 0 680.408 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 (323 /sec) c decisions : 389823 (573 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 680.208 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.93 0.97 0.94 2/54 9474 Raw data (stat): 9474 (runsolver) R 9473 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782084105 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.0003 s] Raw data (loadavg): 0.94 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0005 s] Raw data (loadavg): 0.95 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0004 s] Raw data (loadavg): 0.95 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0007 s] Raw data (loadavg): 0.96 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0009 s] Raw data (loadavg): 0.97 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.001 s] Raw data (loadavg): 0.97 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0017 s] Raw data (loadavg): 0.97 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0022 s] Raw data (loadavg): 0.98 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0023 s] Raw data (loadavg): 0.98 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.003 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.004 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.004 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.005 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.005 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.005 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.005 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.005 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.012 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.012 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.351 s] Raw data (loadavg): 0.99 0.97 0.94 1/53 9478 Raw data (stat): 9474 (minisat+_script) S 9473 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782084105 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 30 Real time (s): 680.351 CPU time (s): 680.408 CPU user time (s): 680.224 CPU system time (s): 0.183972 CPU usage (%): 100.008 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 207 #### END VERIFIER DATA ####