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 wulflinc26 THE 2005-04-14 02:07:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4288 boxname=wulflinc26 idbench=152 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b78d16df5ec546c41fce5f9f07c0fd92 /oldhome/oroussel/tmp/wulflinc26/normalized-ii32c2.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-ii32c2.opb /oldhome/oroussel/tmp/wulflinc26/normalized-ii32c2.opb IDLAUNCH: 4288 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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 : 3 cpu MHz : 451.061 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 834808 kB Buffers: 35268 kB Cached: 124504 kB SwapCached: 2476 kB Active: 55640 kB Inactive: 109528 kB HighTotal: 131008 kB HighFree: 3416 kB LowTotal: 903652 kB LowFree: 831392 kB SwapTotal: 2097892 kB SwapFree: 2095416 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6948 kB Slab: 29272 kB Committed_AS: 63604 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 02:19:19 (client local time) WITH STATUS 30 IN 680.248 SECONDS stats: 4288 0 680.248 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 (323 /sec) c decisions : 389823 (573 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 680.022 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.92 0.98 0.93 2/54 29165 Raw data (stat): 29165 (runsolver) R 29164 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480874329 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0004 s] Raw data (loadavg): 0.93 0.98 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 1942 0 0 0 992 6 0 0 25 0 1 0 480874329 9871360 1916 4294967295 134512640 134672761 3221224560 3221223664 134559896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2410 1916 603 41 0 2369 0 vsize: 9640 [startup+20.0015 s] Raw data (loadavg): 0.94 0.98 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 2439 0 0 0 1990 8 0 0 25 0 1 0 480874329 11886592 2413 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2902 2413 603 41 0 2861 0 vsize: 11608 [startup+30.0022 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 2760 0 0 0 2988 9 0 0 25 0 1 0 480874329 13221888 2734 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3228 2734 603 41 0 3187 0 vsize: 12912 [startup+40.0013 s] Raw data (loadavg): 0.96 0.98 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3036 0 0 0 3987 10 0 0 25 0 1 0 480874329 14450688 3010 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3528 3010 603 41 0 3487 0 vsize: 14112 [startup+50.0025 s] Raw data (loadavg): 0.96 0.98 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3318 0 0 0 4985 11 0 0 25 0 1 0 480874329 15519744 3292 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3789 3292 603 41 0 3748 0 vsize: 15156 [startup+60.0032 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3579 0 0 0 5983 13 0 0 25 0 1 0 480874329 16580608 3553 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4048 3553 603 41 0 4007 0 vsize: 16192 [startup+70.0035 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3846 0 0 0 6982 14 0 0 25 0 1 0 480874329 17637376 3820 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4306 3820 603 41 0 4265 0 vsize: 17224 [startup+80.0046 s] Raw data (loadavg): 1.06 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3968 0 0 0 7981 15 0 0 25 0 1 0 480874329 18169856 3942 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4436 3942 603 41 0 4395 0 vsize: 17744 [startup+90.0041 s] Raw data (loadavg): 1.05 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3968 0 0 0 8981 16 0 0 25 0 1 0 480874329 18169856 3942 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3942 603 41 0 4395 0 vsize: 17744 [startup+100.004 s] Raw data (loadavg): 1.04 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3968 0 0 0 9981 16 0 0 25 0 1 0 480874329 18169856 3942 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3942 603 41 0 4395 0 vsize: 17744 [startup+110.004 s] Raw data (loadavg): 1.03 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3968 0 0 0 10981 16 0 0 25 0 1 0 480874329 18169856 3942 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3942 603 41 0 4395 0 vsize: 17744 [startup+120.005 s] Raw data (loadavg): 1.03 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3968 0 0 0 11981 16 0 0 25 0 1 0 480874329 18169856 3942 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3942 603 41 0 4395 0 vsize: 17744 [startup+130.004 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3972 0 0 0 12981 16 0 0 25 0 1 0 480874329 18169856 3946 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3946 603 41 0 4395 0 vsize: 17744 [startup+140.004 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3972 0 0 0 13981 16 0 0 25 0 1 0 480874329 18169856 3946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3946 603 41 0 4395 0 vsize: 17744 [startup+150.005 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3978 0 0 0 14981 16 0 0 25 0 1 0 480874329 18169856 3952 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3952 603 41 0 4395 0 vsize: 17744 [startup+160.004 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 15982 16 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+170.005 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 16982 16 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+180.006 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 17982 16 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+190.006 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 18982 16 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+200.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 19982 16 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+210.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 20982 16 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+220.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 21982 17 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223744 134559509 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+230.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 22982 17 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223664 134560285 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+240.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 23982 17 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+250.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3979 0 0 0 24982 17 0 0 25 0 1 0 480874329 18169856 3953 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3953 603 41 0 4395 0 vsize: 17744 [startup+260.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 25982 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223696 134565078 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+270.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 26983 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+280.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 27983 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+290.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 28983 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+300.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 29983 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+310.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 30983 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+320.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 31984 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+330.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 32984 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223664 134560034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+340.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 33984 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+350.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 34984 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+360.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 35984 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+370.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 36984 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+380.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3980 0 0 0 37984 17 0 0 25 0 1 0 480874329 18169856 3954 4294967295 134512640 134672761 3221224560 3221223744 134558360 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3954 603 41 0 4395 0 vsize: 17744 [startup+390.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3981 0 0 0 38984 18 0 0 25 0 1 0 480874329 18169856 3955 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3955 603 41 0 4395 0 vsize: 17744 [startup+400.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3981 0 0 0 39984 18 0 0 25 0 1 0 480874329 18169856 3955 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3955 603 41 0 4395 0 vsize: 17744 [startup+410.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3981 0 0 0 40984 18 0 0 25 0 1 0 480874329 18169856 3955 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3955 603 41 0 4395 0 vsize: 17744 [startup+420.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3981 0 0 0 41985 18 0 0 25 0 1 0 480874329 18169856 3955 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3955 603 41 0 4395 0 vsize: 17744 [startup+430.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3981 0 0 0 42985 18 0 0 25 0 1 0 480874329 18169856 3955 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3955 603 41 0 4395 0 vsize: 17744 [startup+440.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3984 0 0 0 43985 18 0 0 25 0 1 0 480874329 18169856 3958 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4436 3958 603 41 0 4395 0 vsize: 17744 [startup+450.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3990 0 0 0 44985 18 0 0 25 0 1 0 480874329 18317312 3964 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3964 603 41 0 4431 0 vsize: 17888 [startup+460.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3996 0 0 0 45985 18 0 0 25 0 1 0 480874329 18317312 3970 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3970 603 41 0 4431 0 vsize: 17888 [startup+470.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3997 0 0 0 46985 18 0 0 25 0 1 0 480874329 18317312 3971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3971 603 41 0 4431 0 vsize: 17888 [startup+480.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3997 0 0 0 47986 18 0 0 25 0 1 0 480874329 18317312 3971 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3971 603 41 0 4431 0 vsize: 17888 [startup+490.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3998 0 0 0 48986 18 0 0 25 0 1 0 480874329 18317312 3972 4294967295 134512640 134672761 3221224560 3221223664 134560344 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3972 603 41 0 4431 0 vsize: 17888 [startup+500.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3998 0 0 0 49986 18 0 0 25 0 1 0 480874329 18317312 3972 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3972 603 41 0 4431 0 vsize: 17888 [startup+510.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3998 0 0 0 50986 18 0 0 25 0 1 0 480874329 18317312 3972 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3972 603 41 0 4431 0 vsize: 17888 [startup+520.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3998 0 0 0 51986 18 0 0 25 0 1 0 480874329 18317312 3972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3972 603 41 0 4431 0 vsize: 17888 [startup+530.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3998 0 0 0 52987 18 0 0 25 0 1 0 480874329 18317312 3972 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3972 603 41 0 4431 0 vsize: 17888 [startup+540.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3998 0 0 0 53987 18 0 0 25 0 1 0 480874329 18317312 3972 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3972 603 41 0 4431 0 vsize: 17888 [startup+550.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 3998 0 0 0 54987 18 0 0 25 0 1 0 480874329 18317312 3972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3972 603 41 0 4431 0 vsize: 17888 [startup+560.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4010 0 0 0 55987 18 0 0 25 0 1 0 480874329 18317312 3984 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4472 3984 603 41 0 4431 0 vsize: 17888 [startup+570.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4068 0 0 0 56987 18 0 0 25 0 1 0 480874329 18579456 4042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4536 4042 603 41 0 4495 0 vsize: 18144 [startup+580.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4315 0 0 0 57986 19 0 0 25 0 1 0 480874329 19779584 4289 4294967295 134512640 134672761 3221224560 3221223760 134557916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4829 4289 603 41 0 4788 0 vsize: 19316 [startup+590.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4515 0 0 0 58986 20 0 0 25 0 1 0 480874329 20578304 4489 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4489 603 41 0 4983 0 vsize: 20096 [startup+600.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4517 0 0 0 59986 20 0 0 25 0 1 0 480874329 20578304 4491 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4491 603 41 0 4983 0 vsize: 20096 [startup+610.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4529 0 0 0 60986 20 0 0 25 0 1 0 480874329 20578304 4503 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4503 603 41 0 4983 0 vsize: 20096 [startup+620.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4533 0 0 0 61986 20 0 0 25 0 1 0 480874329 20578304 4507 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4507 603 41 0 4983 0 vsize: 20096 [startup+630.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4535 0 0 0 62986 20 0 0 25 0 1 0 480874329 20578304 4509 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4509 603 41 0 4983 0 vsize: 20096 [startup+640.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4535 0 0 0 63986 20 0 0 25 0 1 0 480874329 20578304 4509 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4509 603 41 0 4983 0 vsize: 20096 [startup+650.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4535 0 0 0 64987 20 0 0 25 0 1 0 480874329 20578304 4509 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4509 603 41 0 4983 0 vsize: 20096 [startup+660.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4540 0 0 0 65986 20 0 0 25 0 1 0 480874329 20578304 4514 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5024 4514 603 41 0 4983 0 vsize: 20096 [startup+670.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4544 0 0 0 66987 20 0 0 25 0 1 0 480874329 20721664 4518 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5059 4518 603 41 0 5018 0 vsize: 20236 [startup+680.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4552 0 0 0 67987 20 0 0 25 0 1 0 480874329 20721664 4526 4294967295 134512640 134672761 3221224560 3221223712 134554673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5059 4526 603 41 0 5018 0 vsize: 20236 [startup+680.183 s] Raw data (loadavg): 1.00 1.00 0.93 1/53 29165 Raw data (stat): 29165 (minisat+) R 29164 22612 22611 0 -1 0 4552 0 0 0 67987 20 0 0 25 0 1 0 480874329 20721664 4526 4294967295 134512640 134672761 3221224560 3221223712 134554673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5059 4526 603 41 0 5018 0 vsize: 0 Child status: 30 Real time (s): 680.183 CPU time (s): 680.248 CPU user time (s): 680.032 CPU system time (s): 0.215967 CPU usage (%): 100.009 Max. virtual memory (Kb): 20236 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 207 #### END VERIFIER DATA ####