Name | 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 | YES |
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 | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 698.131 |
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 |
LAUNCH ON wulflinc4 THE 2005-09-18 15:19:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2489 boxname=wulflinc4 idbench=145 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b78d16df5ec546c41fce5f9f07c0fd92 /oldhome/oroussel/tmp/wulflinc4/normalized-ii32c2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-ii32c2.opb IDLAUNCH: 2489 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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 : 451.169 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: 924120 kB Buffers: 34484 kB Cached: 52480 kB SwapCached: 960 kB Active: 64280 kB Inactive: 25336 kB HighTotal: 131008 kB HighFree: 76188 kB LowTotal: 903652 kB LowFree: 847932 kB SwapTotal: 2097136 kB SwapFree: 2095628 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5692 kB Slab: 15360 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 15:31:14 (client local time) WITH STATUS 30 IN 698.131 SECONDS stats: 2489 0 698.131 30
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 (315 /sec) c decisions : 389823 (559 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 697.754 s c _______________________________________________________________________________
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/14171/stat): 14171 (minisat+_script) R 14170 14171 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784041517 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14171/statm): 174 3 169 147 0 27 0 [pid=14171] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=14172 New process pid=14173 New process pid=14174 execve syscall for /bin/sed executable One traced child (pid=14173) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=14174) exited with status: 0 One traced child (pid=14172) exited with status: 0 New process pid=14175 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-ii32c2.opb [startup+10.0032 s] Raw data (loadavg): 0.93 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 1784 0 0 0 978 8 0 0 25 0 1 0 1784041522 7917568 1767 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 1933 1767 145 145 0 1788 0 [pid=14175] vsize: 7732 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 9856 [startup+20.0051 s] Raw data (loadavg): 0.94 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 2282 0 0 0 1968 12 0 0 25 0 1 0 1784041522 9973760 2265 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 2435 2265 145 145 0 2290 0 [pid=14175] vsize: 9740 Current children cumulated CPU time (s) 19.82 Current children cumulated vsize (Kb) 11864 [startup+30.0059 s] Raw data (loadavg): 0.95 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 2600 0 0 0 2962 15 0 0 25 0 1 0 1784041522 11264000 2583 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 2750 2583 145 145 0 2605 0 [pid=14175] vsize: 11000 Current children cumulated CPU time (s) 29.79 Current children cumulated vsize (Kb) 13124 [startup+40.0058 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 2861 0 0 0 3958 17 0 0 25 0 1 0 1784041522 12324864 2844 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3009 2844 145 145 0 2864 0 [pid=14175] vsize: 12036 Current children cumulated CPU time (s) 39.77 Current children cumulated vsize (Kb) 14160 [startup+50.0076 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3156 0 0 0 4953 20 0 0 25 0 1 0 1784041522 13582336 3139 4294967295 134512640 135094434 3221224448 3221223040 134556859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3316 3139 145 145 0 3171 0 [pid=14175] vsize: 13264 Current children cumulated CPU time (s) 49.75 Current children cumulated vsize (Kb) 15388 [startup+60.0085 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3402 0 0 0 5948 22 0 0 25 0 1 0 1784041522 14577664 3385 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3559 3385 145 145 0 3414 0 [pid=14175] vsize: 14236 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 16360 [startup+70.0104 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3670 0 0 0 6942 25 0 0 25 0 1 0 1784041522 15667200 3653 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3825 3653 145 145 0 3680 0 [pid=14175] vsize: 15300 Current children cumulated CPU time (s) 69.69 Current children cumulated vsize (Kb) 17424 [startup+80.0112 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3832 0 0 0 7940 26 0 0 25 0 1 0 1784041522 16322560 3815 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3985 3815 145 145 0 3840 0 [pid=14175] vsize: 15940 Current children cumulated CPU time (s) 79.68 Current children cumulated vsize (Kb) 18064 [startup+90.0121 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3832 0 0 0 8940 26 0 0 25 0 1 0 1784041522 16322560 3815 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3985 3815 145 145 0 3840 0 [pid=14175] vsize: 15940 Current children cumulated CPU time (s) 89.68 Current children cumulated vsize (Kb) 18064 [startup+100.013 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3832 0 0 0 9940 26 0 0 25 0 1 0 1784041522 16322560 3815 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3985 3815 145 145 0 3840 0 [pid=14175] vsize: 15940 Current children cumulated CPU time (s) 99.68 Current children cumulated vsize (Kb) 18064 [startup+110.014 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3832 0 0 0 10940 26 0 0 25 0 1 0 1784041522 16322560 3815 4294967295 134512640 135094434 3221224448 3221223104 134556602 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3985 3815 145 145 0 3840 0 [pid=14175] vsize: 15940 Current children cumulated CPU time (s) 109.68 Current children cumulated vsize (Kb) 18064 [startup+120.016 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3832 0 0 0 11941 26 0 0 25 0 1 0 1784041522 16322560 3815 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3985 3815 145 145 0 3840 0 [pid=14175] vsize: 15940 Current children cumulated CPU time (s) 119.69 Current children cumulated vsize (Kb) 18064 [startup+130.016 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3833 0 0 0 12941 26 0 0 25 0 1 0 1784041522 16322560 3816 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3985 3816 145 145 0 3840 0 [pid=14175] vsize: 15940 Current children cumulated CPU time (s) 129.69 Current children cumulated vsize (Kb) 18064 [startup+140.017 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3833 0 0 0 13940 26 0 0 25 0 1 0 1784041522 16322560 3816 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14175/statm): 3985 3816 145 145 0 3840 0 [pid=14175] vsize: 15940 Current children cumulated CPU time (s) 139.68 Current children cumulated vsize (Kb) 18064 [startup+150.019 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3838 0 0 0 14940 26 0 0 25 0 1 0 1784041522 16355328 3821 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3821 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 149.68 Current children cumulated vsize (Kb) 18096 [startup+160.02 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 15940 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 159.68 Current children cumulated vsize (Kb) 18096 [startup+170.021 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 16941 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 169.69 Current children cumulated vsize (Kb) 18096 [startup+180.022 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 17941 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 179.69 Current children cumulated vsize (Kb) 18096 [startup+190.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 18941 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 189.69 Current children cumulated vsize (Kb) 18096 [startup+200.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 19941 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 199.69 Current children cumulated vsize (Kb) 18096 [startup+210.024 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 20941 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 209.69 Current children cumulated vsize (Kb) 18096 [startup+220.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 21942 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 219.7 Current children cumulated vsize (Kb) 18096 [startup+230.027 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 22942 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 229.7 Current children cumulated vsize (Kb) 18096 [startup+240.028 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 23942 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 239.7 Current children cumulated vsize (Kb) 18096 [startup+250.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3839 0 0 0 24942 26 0 0 25 0 1 0 1784041522 16355328 3822 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3822 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 249.7 Current children cumulated vsize (Kb) 18096 [startup+260.03 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 25942 26 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223040 134556914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 259.7 Current children cumulated vsize (Kb) 18096 [startup+270.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 26942 26 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 269.7 Current children cumulated vsize (Kb) 18096 [startup+280.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 27943 26 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 279.71 Current children cumulated vsize (Kb) 18096 [startup+290.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 28943 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 289.72 Current children cumulated vsize (Kb) 18096 [startup+300.033 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 29943 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 299.72 Current children cumulated vsize (Kb) 18096 [startup+310.034 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 30943 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 309.72 Current children cumulated vsize (Kb) 18096 [startup+320.035 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 31944 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223040 134557199 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 319.73 Current children cumulated vsize (Kb) 18096 [startup+330.036 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 32944 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 329.73 Current children cumulated vsize (Kb) 18096 [startup+340.036 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 33944 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223040 134557271 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 339.73 Current children cumulated vsize (Kb) 18096 [startup+350.037 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 34944 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 349.73 Current children cumulated vsize (Kb) 18096 [startup+360.038 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 35944 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 359.73 Current children cumulated vsize (Kb) 18096 [startup+370.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 36945 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 369.74 Current children cumulated vsize (Kb) 18096 [startup+380.04 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 37945 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 379.74 Current children cumulated vsize (Kb) 18096 [startup+390.041 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 38945 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 389.74 Current children cumulated vsize (Kb) 18096 [startup+400.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3840 0 0 0 39945 27 0 0 25 0 1 0 1784041522 16355328 3823 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3823 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 399.74 Current children cumulated vsize (Kb) 18096 [startup+410.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3841 0 0 0 40946 27 0 0 25 0 1 0 1784041522 16355328 3824 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3824 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 409.75 Current children cumulated vsize (Kb) 18096 [startup+420.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3841 0 0 0 41946 27 0 0 25 0 1 0 1784041522 16355328 3824 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3824 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 419.75 Current children cumulated vsize (Kb) 18096 [startup+430.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3841 0 0 0 42946 27 0 0 25 0 1 0 1784041522 16355328 3824 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3824 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 429.75 Current children cumulated vsize (Kb) 18096 [startup+440.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3841 0 0 0 43946 27 0 0 25 0 1 0 1784041522 16355328 3824 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3824 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 439.75 Current children cumulated vsize (Kb) 18096 [startup+450.046 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3843 0 0 0 44946 27 0 0 25 0 1 0 1784041522 16355328 3826 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 3993 3826 145 145 0 3848 0 [pid=14175] vsize: 15972 Current children cumulated CPU time (s) 449.75 Current children cumulated vsize (Kb) 18096 [startup+460.047 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3849 0 0 0 45947 27 0 0 25 0 1 0 1784041522 16388096 3832 4294967295 134512640 135094434 3221224448 3221223120 134556078 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4001 3832 145 145 0 3856 0 [pid=14175] vsize: 16004 Current children cumulated CPU time (s) 459.76 Current children cumulated vsize (Kb) 18128 [startup+470.048 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3855 0 0 0 46947 27 0 0 25 0 1 0 1784041522 16420864 3838 4294967295 134512640 135094434 3221224448 3221223072 134562122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3838 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 469.76 Current children cumulated vsize (Kb) 18160 [startup+480.048 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3856 0 0 0 47947 27 0 0 25 0 1 0 1784041522 16420864 3839 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3839 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 479.76 Current children cumulated vsize (Kb) 18160 [startup+490.049 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 48947 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221223108 134553454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 489.76 Current children cumulated vsize (Kb) 18160 [startup+500.05 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 49948 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221223120 134556526 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 499.77 Current children cumulated vsize (Kb) 18160 [startup+510.051 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 50948 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 509.77 Current children cumulated vsize (Kb) 18160 [startup+520.052 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 51948 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221222992 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 519.77 Current children cumulated vsize (Kb) 18160 [startup+530.053 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 52948 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 529.77 Current children cumulated vsize (Kb) 18160 [startup+540.054 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 53948 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 539.77 Current children cumulated vsize (Kb) 18160 [startup+550.054 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 54949 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 549.78 Current children cumulated vsize (Kb) 18160 [startup+560.055 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3857 0 0 0 55949 27 0 0 25 0 1 0 1784041522 16420864 3840 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4009 3840 145 145 0 3864 0 [pid=14175] vsize: 16036 Current children cumulated CPU time (s) 559.78 Current children cumulated vsize (Kb) 18160 [startup+570.056 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3863 0 0 0 56949 27 0 0 25 0 1 0 1784041522 16453632 3846 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4017 3846 145 145 0 3872 0 [pid=14175] vsize: 16068 Current children cumulated CPU time (s) 569.78 Current children cumulated vsize (Kb) 18192 [startup+580.057 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 3876 0 0 0 57949 27 0 0 25 0 1 0 1784041522 16519168 3859 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4033 3859 145 145 0 3888 0 [pid=14175] vsize: 16132 Current children cumulated CPU time (s) 579.78 Current children cumulated vsize (Kb) 18256 [startup+590.058 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4077 0 0 0 58945 28 0 0 25 0 1 0 1784041522 17342464 4060 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4234 4060 145 145 0 4089 0 [pid=14175] vsize: 16936 Current children cumulated CPU time (s) 589.75 Current children cumulated vsize (Kb) 19060 [startup+600.06 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4291 0 0 0 59942 31 0 0 25 0 1 0 1784041522 18337792 4274 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4477 4274 145 145 0 4332 0 [pid=14175] vsize: 17908 Current children cumulated CPU time (s) 599.75 Current children cumulated vsize (Kb) 20032 [startup+610.061 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4379 0 0 0 60941 31 0 0 25 0 1 0 1784041522 18694144 4362 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4564 4362 145 145 0 4419 0 [pid=14175] vsize: 18256 Current children cumulated CPU time (s) 609.74 Current children cumulated vsize (Kb) 20380 [startup+620.062 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4384 0 0 0 61941 31 0 0 25 0 1 0 1784041522 18718720 4367 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4570 4367 145 145 0 4425 0 [pid=14175] vsize: 18280 Current children cumulated CPU time (s) 619.74 Current children cumulated vsize (Kb) 20404 [startup+630.063 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4390 0 0 0 62942 31 0 0 25 0 1 0 1784041522 18751488 4373 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4578 4373 145 145 0 4433 0 [pid=14175] vsize: 18312 Current children cumulated CPU time (s) 629.75 Current children cumulated vsize (Kb) 20436 [startup+640.064 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4397 0 0 0 63942 31 0 0 25 0 1 0 1784041522 18776064 4380 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4584 4380 145 145 0 4439 0 [pid=14175] vsize: 18336 Current children cumulated CPU time (s) 639.75 Current children cumulated vsize (Kb) 20460 [startup+650.065 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4397 0 0 0 64942 31 0 0 25 0 1 0 1784041522 18776064 4380 4294967295 134512640 135094434 3221224448 3221223072 134562070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4584 4380 145 145 0 4439 0 [pid=14175] vsize: 18336 Current children cumulated CPU time (s) 649.75 Current children cumulated vsize (Kb) 20460 [startup+660.066 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4397 0 0 0 65942 31 0 0 25 0 1 0 1784041522 18776064 4380 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4584 4380 145 145 0 4439 0 [pid=14175] vsize: 18336 Current children cumulated CPU time (s) 659.75 Current children cumulated vsize (Kb) 20460 [startup+670.068 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4397 0 0 0 66942 31 0 0 25 0 1 0 1784041522 18776064 4380 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4584 4380 145 145 0 4439 0 [pid=14175] vsize: 18336 Current children cumulated CPU time (s) 669.75 Current children cumulated vsize (Kb) 20460 [startup+680.069 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4401 0 0 0 67941 32 0 0 25 0 1 0 1784041522 18792448 4384 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14175/statm): 4588 4384 145 145 0 4443 0 [pid=14175] vsize: 18352 Current children cumulated CPU time (s) 679.75 Current children cumulated vsize (Kb) 20476 [startup+690.069 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 14175 Raw data (/proc/14171/stat): 14171 (minisat+_script) S 14170 14171 6847 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1784041517 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14171/statm): 531 226 485 147 0 384 0 [pid=14171] vsize: 2124 Raw data (/proc/14175/stat): 14175 (minisat+_64-bit) R 14171 14171 6847 0 -1 0 4408 0 0 0 68940 32 0 0 25 0 1 0 1784041522 18825216 4391 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14175/statm): 4596 4391 145 145 0 4451 0 [pid=14175] vsize: 18384 Current children cumulated CPU time (s) 689.74 Current children cumulated vsize (Kb) 20508 One traced child (pid=14175) exited with status: 30 One traced child (pid=14171) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 698.442 CPU time (s): 698.131 CPU user time (s): 697.768 CPU system time (s): 0.362944 CPU usage (%): 99.9554 Max. virtual memory (cumulated for all children) (Kb): 20508
Verifier: OK 207