Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-share2b.opb |
MD5SUM | 093811c51770a4a5a69679d486994a51 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 580 |
Biggest coefficient in the objective function | 199229440 |
Number of bits for the biggest coefficient in the objective function | 28 |
Sum of the numbers in the objective function | 4428132225 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 540016640 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 10719582225 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 1580 |
Total number of constraints | 96 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 96 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 240 |
LAUNCH ON wulflinc30 THE 2005-09-20 02:54:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3198 boxname=wulflinc30 idbench=854 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 093811c51770a4a5a69679d486994a51 /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-share2b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-share2b.opb IDLAUNCH: 3198 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 868120 kB Buffers: 27760 kB Cached: 109052 kB SwapCached: 752 kB Active: 32596 kB Inactive: 106792 kB HighTotal: 131008 kB HighFree: 28028 kB LowTotal: 903652 kB LowFree: 840092 kB SwapTotal: 2097892 kB SwapFree: 2096620 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 21604 kB Committed_AS: 64268 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:14:44 (client local time) WITH STATUS 0 IN 1206.98 SECONDS stats: 3198 7 1206.98 0
c Parsing PB file... c Converting 109 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############# c -- Clauses(.)/Splits(s): (none) c ---[ 108]---> Adder-cost: 674 maxlim: 3085667 bits: 23/22 c ---[ 107]---> Adder-cost: 446 maxlim: 729572 bits: 21/20 c ---[ 106]---> Adder-cost: 486 maxlim: 819149 bits: 21/20 c ---[ 105]---> Adder-cost: 668 maxlim: 1474469 bits: 22/21 c ---[ 104]---> Adder-cost: 1206 maxlim: 16382999 bits: 25/24 c ---[ 103]---> Adder-cost: 1198 maxlim: 16382999 bits: 25/24 c ---[ 102]---> Adder-cost: 1012 maxlim: 14744699 bits: 25/24 c ---[ 101]---> Adder-cost: 794 maxlim: 14744699 bits: 25/24 c ---[ 100]---> BDD-cost: 130 c ---[ 98]---> Sorter-cost: 1683 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 97]---> Adder-cost: 532 maxlim: 996050 bits: 21/20 c ---[ 96]---> Adder-cost: 374 maxlim: 367899 bits: 20/19 c ---[ 95]---> Adder-cost: 349 maxlim: 204749 bits: 19/18 c ---[ 94]---> Adder-cost: 511 maxlim: 368549 bits: 20/19 c ---[ 93]---> Adder-cost: 917 maxlim: 3644549 bits: 23/22 c ---[ 92]---> Adder-cost: 931 maxlim: 3644549 bits: 23/22 c ---[ 91]---> Adder-cost: 663 maxlim: 3357899 bits: 23/22 c ---[ 90]---> Adder-cost: 603 maxlim: 3357899 bits: 23/22 c ---[ 89]---> BDD-cost: 110 c ---[ 87]---> Sorter-cost: 1122 Base: 2 2 2 2 2 2 2 2 2 c ---[ 86]---> Adder-cost: 920 maxlim: 2024495 bits: 22/21 c ---[ 85]---> Adder-cost: 574 maxlim: 620838 bits: 20/20 c ---[ 84]---> Adder-cost: 595 maxlim: 409549 bits: 20/19 c ---[ 83]---> Adder-cost: 744 maxlim: 737189 bits: 21/20 c ---[ 82]---> Adder-cost: 1349 maxlim: 8190999 bits: 24/23 c ---[ 81]---> Adder-cost: 1287 maxlim: 8190999 bits: 24/23 c ---[ 80]---> Adder-cost: 1003 maxlim: 3685949 bits: 23/22 c ---[ 79]---> Adder-cost: 935 maxlim: 7371899 bits: 24/23 c ---[ 78]---> BDD-cost: 120 c ---[ 76]---> Adder-cost: 188 maxlim: 12022 bits: 15/14 c ---[ 75]---> Adder-cost: 740 maxlim: 1234840 bits: 21/21 c ---[ 74]---> Adder-cost: 482 maxlim: 466030 bits: 20/19 c ---[ 73]---> Adder-cost: 580 maxlim: 204749 bits: 19/18 c ---[ 72]---> Adder-cost: 559 maxlim: 368549 bits: 20/19 c ---[ 71]---> Adder-cost: 1158 maxlim: 3644549 bits: 23/22 c ---[ 70]---> Adder-cost: 1072 maxlim: 3644549 bits: 23/22 c ---[ 69]---> Adder-cost: 863 maxlim: 3357899 bits: 23/22 c ---[ 68]---> Adder-cost: 829 maxlim: 3357899 bits: 23/22 c ---[ 67]---> BDD-cost: 110 c ---[ 65]---> Sorter-cost: 1671 Base: 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Adder-cost: 668 maxlim: 1289301 bits: 21/21 c ---[ 63]---> Adder-cost: 348 maxlim: 438007 bits: 20/19 c ---[ 62]---> Adder-cost: 526 maxlim: 204749 bits: 19/18 c ---[ 61]---> Adder-cost: 714 maxlim: 368549 bits: 20/19 c ---[ 60]---> Adder-cost: 1214 maxlim: 4135949 bits: 23/22 c ---[ 59]---> Adder-cost: 1141 maxlim: 4135949 bits: 23/22 c ---[ 58]---> Adder-cost: 1048 maxlim: 3726449 bits: 23/22 c ---[ 57]---> Adder-cost: 998 maxlim: 3726449 bits: 23/22 c ---[ 56]---> BDD-cost: 110 c ---[ 54]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Adder-cost: 686 maxlim: 1802920 bits: 22/21 c ---[ 52]---> Adder-cost: 424 maxlim: 482951 bits: 20/19 c ---[ 51]---> Adder-cost: 443 maxlim: 409549 bits: 20/19 c ---[ 50]---> Adder-cost: 626 maxlim: 737189 bits: 21/20 c ---[ 49]---> Adder-cost: 1179 maxlim: 7289989 bits: 24/23 c ---[ 48]---> Adder-cost: 1207 maxlim: 7289989 bits: 24/23 c ---[ 47]---> Adder-cost: 941 maxlim: 6716619 bits: 24/23 c ---[ 46]---> Adder-cost: 1025 maxlim: 6716619 bits: 24/23 c ---[ 45]---> BDD-cost: 120 c ---[ 43]---> Sorter-cost: 1872 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 348 Base: 2 2 2 2 2 2 2 2 2 c ---[ 41]---> BDD-cost: 43 c ---[ 40]---> Sorter-cost: 1411 Base: 2 2 2 2 2 2 2 2 5 2 c ---[ 39]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> BDD-cost: 38 c ---[ 37]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 c ---[ 36]---> BDD-cost: 38 c ---[ 35]---> Sorter-cost: 2296 Base: 2 2 2 2 2 2 2 2 5 2 c ---[ 34]---> BDD-cost: 7 c ---[ 33]---> BDD-cost: 7 c ---[ 32]---> Sorter-cost: 226 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 226 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 226 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Adder-cost: 288 maxlim: 120508 bits: 18/17 c ---[ 28]---> BDD-cost: 33 c ---[ 27]---> BDD-cost: 33 c ---[ 26]---> BDD-cost: 33 c ---[ 25]---> BDD-cost: 7 c ---[ 23]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> BDD-cost: 116 c ---[ 19]---> Sorter-cost: 261 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> BDD-cost: 106 c ---[ 13]---> BDD-cost: 101 c ---[ 12]---> BDD-cost: 33 c ---[ 11]---> Sorter-cost: 615 Base: 2 2 2 2 2 2 2 2 2 3 c ---[ 10]---> Adder-cost: 662 maxlim: 5316026 bits: 24/23 c ---[ 9]---> Adder-cost: 488 maxlim: 1103265 bits: 22/21 c ---[ 8]---> Adder-cost: 532 maxlim: 1638349 bits: 22/21 c ---[ 7]---> Adder-cost: 674 maxlim: 2949029 bits: 23/22 c ---[ 6]---> Adder-cost: 1252 maxlim: 29490299 bits: 26/25 c ---[ 5]---> Adder-cost: 1262 maxlim: 29490299 bits: 26/25 c ---[ 4]---> Adder-cost: 1116 maxlim: 27196609 bits: 26/25 c ---[ 3]---> Adder-cost: 1156 maxlim: 27196609 bits: 26/25 c ---[ 2]---> BDD-cost: 140 c ---[ 0]---> Sorter-cost: 1996 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 360893 1236415 | 120297 0 0 nan | 0.000 % | c | 101 | 360878 1236379 | 132326 98 380 3.9 | 2.873 % | c | 251 | 360811 1236231 | 145559 239 958 4.0 | 2.908 % | c | 476 | 360760 1236116 | 160115 455 3013 6.6 | 2.924 % | c | 815 | 360760 1236116 | 176126 794 8568 10.8 | 2.924 % | c | 1322 | 360737 1236064 | 193739 1298 17079 13.2 | 2.933 % | c | 2082 | 360737 1236064 | 213113 2058 38721 18.8 | 2.933 % | c | 3221 | 360720 1236023 | 234424 3194 73068 22.9 | 2.940 % | c | 4929 | 360713 1236000 | 257867 4901 121305 24.8 | 2.941 % | c | 7491 | 360304 1234737 | 283654 7450 188354 25.3 | 3.016 % | c | 11335 | 360304 1234737 | 312019 11294 355985 31.5 | 3.016 % | c | 17101 | 360293 1234713 | 343221 17059 536414 31.4 | 3.021 % | c | 25750 | 360293 1234713 | 377543 25708 728286 28.3 | 3.021 % | c | 38725 | 360248 1234613 | 415297 38678 1438073 37.2 | 3.041 % | c | 58187 | 360093 1234269 | 456827 58114 2248367 38.7 | 3.110 % | c | 87379 | 359916 1233869 | 502510 87285 3739751 42.8 | 3.186 % | c | 131168 | 359684 1233325 | 552761 131036 6184994 47.2 | 3.278 % | c | 196852 | 359631 1233205 | 608037 196697 9696489 49.3 | 3.302 % | c | 295378 | 359501 1232901 | 668841 295218 16644495 56.4 | 3.369 % |
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/3153/stat): 3153 (minisat+_script) R 3152 3153 5245 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855082174 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/3153/statm): 174 3 169 147 0 27 0 [pid=3153] 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=3154 New process pid=3155 New process pid=3156 execve syscall for /bin/sed executable One traced child (pid=3155) 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=3156) exited with status: 0 One traced child (pid=3154) exited with status: 0 New process pid=3157 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-share2b.opb [startup+10.0038 s] Raw data (loadavg): 0.67 0.22 0.07 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 704 0 0 0 988 3 0 0 25 0 1 0 1855082179 2666496 538 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 651 538 145 145 0 506 0 [pid=3157] vsize: 2604 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 4728 [startup+20.0056 s] Raw data (loadavg): 0.72 0.24 0.08 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 865 0 0 0 1987 4 0 0 25 0 1 0 1855082179 2830336 586 4294967295 134512640 135094434 3221224432 3221221432 134676989 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 691 586 145 145 0 546 0 [pid=3157] vsize: 2764 Current children cumulated CPU time (s) 19.91 Current children cumulated vsize (Kb) 4888 [startup+30.0064 s] Raw data (loadavg): 0.76 0.27 0.09 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1084 0 0 0 2985 5 0 0 25 0 1 0 1855082179 3526656 702 4294967295 134512640 135094434 3221224432 3221221904 134676294 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 861 702 145 145 0 716 0 [pid=3157] vsize: 3444 Current children cumulated CPU time (s) 29.9 Current children cumulated vsize (Kb) 5568 [startup+40.0072 s] Raw data (loadavg): 0.80 0.29 0.10 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1421 0 0 0 3982 7 0 0 25 0 1 0 1855082179 4063232 853 4294967295 134512640 135094434 3221224432 3221221376 134677059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 992 853 145 145 0 847 0 [pid=3157] vsize: 3968 Current children cumulated CPU time (s) 39.89 Current children cumulated vsize (Kb) 6092 [startup+50.0079 s] Raw data (loadavg): 0.83 0.31 0.11 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1590 0 0 0 4981 8 0 0 25 0 1 0 1855082179 4337664 951 4294967295 134512640 135094434 3221224432 3221221376 134676259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 1059 951 145 145 0 914 0 [pid=3157] vsize: 4236 Current children cumulated CPU time (s) 49.89 Current children cumulated vsize (Kb) 6360 [startup+60.0087 s] Raw data (loadavg): 0.85 0.33 0.12 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1686 0 0 0 5980 8 0 0 25 0 1 0 1855082179 4399104 976 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 1074 976 145 145 0 929 0 [pid=3157] vsize: 4296 Current children cumulated CPU time (s) 59.88 Current children cumulated vsize (Kb) 6420 [startup+70.0105 s] Raw data (loadavg): 0.88 0.36 0.13 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1831 0 0 0 6979 9 0 0 25 0 1 0 1855082179 5345280 1043 4294967295 134512640 135094434 3221224432 3221221808 134599982 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 1305 1043 145 145 0 1160 0 [pid=3157] vsize: 5220 Current children cumulated CPU time (s) 69.88 Current children cumulated vsize (Kb) 7344 [startup+80.0113 s] Raw data (loadavg): 0.89 0.38 0.14 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1979 0 0 0 7977 10 0 0 25 0 1 0 1855082179 5455872 1094 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 1332 1094 145 145 0 1187 0 [pid=3157] vsize: 5328 Current children cumulated CPU time (s) 79.87 Current children cumulated vsize (Kb) 7452 [startup+90.0131 s] Raw data (loadavg): 0.91 0.40 0.15 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 2428 0 0 0 8975 11 0 0 25 0 1 0 1855082179 6361088 1339 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 1553 1339 145 145 0 1408 0 [pid=3157] vsize: 6212 Current children cumulated CPU time (s) 89.86 Current children cumulated vsize (Kb) 8336 [startup+100.014 s] Raw data (loadavg): 0.92 0.42 0.15 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 2554 0 0 0 9973 12 0 0 25 0 1 0 1855082179 6410240 1359 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 1565 1359 145 145 0 1420 0 [pid=3157] vsize: 6260 Current children cumulated CPU time (s) 99.85 Current children cumulated vsize (Kb) 8384 [startup+110.015 s] Raw data (loadavg): 0.93 0.43 0.16 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 8357 0 0 0 10916 41 0 0 25 0 1 0 1855082179 31309824 7137 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 7644 7137 145 145 0 7499 0 [pid=3157] vsize: 30576 Current children cumulated CPU time (s) 109.57 Current children cumulated vsize (Kb) 32700 [startup+120.016 s] Raw data (loadavg): 0.94 0.45 0.17 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 8823 0 0 0 11907 46 0 0 25 0 1 0 1855082179 33234944 7603 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 8114 7603 145 145 0 7969 0 [pid=3157] vsize: 32456 Current children cumulated CPU time (s) 119.53 Current children cumulated vsize (Kb) 34580 [startup+130.017 s] Raw data (loadavg): 0.95 0.47 0.18 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 9190 0 0 0 12901 48 0 0 25 0 1 0 1855082179 34762752 7970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 8487 7970 145 145 0 8342 0 [pid=3157] vsize: 33948 Current children cumulated CPU time (s) 129.49 Current children cumulated vsize (Kb) 36072 [startup+140.018 s] Raw data (loadavg): 0.96 0.49 0.19 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 9468 0 0 0 13896 51 0 0 25 0 1 0 1855082179 35889152 8248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 8762 8248 145 145 0 8617 0 [pid=3157] vsize: 35048 Current children cumulated CPU time (s) 139.47 Current children cumulated vsize (Kb) 37172 [startup+150.019 s] Raw data (loadavg): 0.96 0.50 0.20 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 9826 0 0 0 14890 53 0 0 25 0 1 0 1855082179 37466112 8606 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 9147 8606 145 145 0 9002 0 [pid=3157] vsize: 36588 Current children cumulated CPU time (s) 149.43 Current children cumulated vsize (Kb) 38712 [startup+160.018 s] Raw data (loadavg): 0.97 0.52 0.20 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 10176 0 0 0 15885 56 0 0 25 0 1 0 1855082179 38879232 8956 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 9492 8956 145 145 0 9347 0 [pid=3157] vsize: 37968 Current children cumulated CPU time (s) 159.41 Current children cumulated vsize (Kb) 40092 [startup+170.019 s] Raw data (loadavg): 0.97 0.53 0.21 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 10585 0 0 0 16877 60 0 0 25 0 1 0 1855082179 40521728 9365 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 9893 9365 145 145 0 9748 0 [pid=3157] vsize: 39572 Current children cumulated CPU time (s) 169.37 Current children cumulated vsize (Kb) 41696 [startup+180.02 s] Raw data (loadavg): 0.98 0.55 0.22 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 10855 0 0 0 17872 62 0 0 25 0 1 0 1855082179 41607168 9635 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 10158 9635 145 145 0 10013 0 [pid=3157] vsize: 40632 Current children cumulated CPU time (s) 179.34 Current children cumulated vsize (Kb) 42756 [startup+190.022 s] Raw data (loadavg): 0.98 0.56 0.23 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 11213 0 0 0 18867 64 0 0 25 0 1 0 1855082179 43048960 9993 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 10510 9993 145 145 0 10365 0 [pid=3157] vsize: 42040 Current children cumulated CPU time (s) 189.31 Current children cumulated vsize (Kb) 44164 [startup+200.023 s] Raw data (loadavg): 0.98 0.58 0.24 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 11575 0 0 0 19861 67 0 0 25 0 1 0 1855082179 44503040 10355 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 10865 10355 145 145 0 10720 0 [pid=3157] vsize: 43460 Current children cumulated CPU time (s) 199.28 Current children cumulated vsize (Kb) 45584 [startup+210.023 s] Raw data (loadavg): 0.98 0.59 0.24 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 11870 0 0 0 20855 69 0 0 25 0 1 0 1855082179 45953024 10650 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 11219 10650 145 145 0 11074 0 [pid=3157] vsize: 44876 Current children cumulated CPU time (s) 209.24 Current children cumulated vsize (Kb) 47000 [startup+220.024 s] Raw data (loadavg): 0.99 0.60 0.25 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 12167 0 0 0 21850 71 0 0 25 0 1 0 1855082179 47104000 10947 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 11500 10947 145 145 0 11355 0 [pid=3157] vsize: 46000 Current children cumulated CPU time (s) 219.21 Current children cumulated vsize (Kb) 48124 [startup+230.025 s] Raw data (loadavg): 0.99 0.62 0.26 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 12446 0 0 0 22845 73 0 0 25 0 1 0 1855082179 48226304 11226 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 11774 11226 145 145 0 11629 0 [pid=3157] vsize: 47096 Current children cumulated CPU time (s) 229.18 Current children cumulated vsize (Kb) 49220 [startup+240.026 s] Raw data (loadavg): 0.99 0.63 0.27 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 12745 0 0 0 23839 75 0 0 25 0 1 0 1855082179 49434624 11525 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 12069 11525 145 145 0 11924 0 [pid=3157] vsize: 48276 Current children cumulated CPU time (s) 239.14 Current children cumulated vsize (Kb) 50400 [startup+250.026 s] Raw data (loadavg): 0.99 0.64 0.27 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13076 0 0 0 24833 78 0 0 25 0 1 0 1855082179 50774016 11856 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 12396 11856 145 145 0 12251 0 [pid=3157] vsize: 49584 Current children cumulated CPU time (s) 249.11 Current children cumulated vsize (Kb) 51708 [startup+260.027 s] Raw data (loadavg): 0.99 0.65 0.28 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13382 0 0 0 25827 80 0 0 25 0 1 0 1855082179 52011008 12162 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 12698 12162 145 145 0 12553 0 [pid=3157] vsize: 50792 Current children cumulated CPU time (s) 259.07 Current children cumulated vsize (Kb) 52916 [startup+270.029 s] Raw data (loadavg): 0.99 0.66 0.29 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13700 0 0 0 26823 82 0 0 25 0 1 0 1855082179 53297152 12480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 13012 12480 145 145 0 12867 0 [pid=3157] vsize: 52048 Current children cumulated CPU time (s) 269.05 Current children cumulated vsize (Kb) 54172 [startup+280.03 s] Raw data (loadavg): 0.99 0.67 0.30 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13963 0 0 0 27816 85 0 0 25 0 1 0 1855082179 54353920 12743 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 13270 12743 145 145 0 13125 0 [pid=3157] vsize: 53080 Current children cumulated CPU time (s) 279.01 Current children cumulated vsize (Kb) 55204 [startup+290.032 s] Raw data (loadavg): 0.99 0.68 0.30 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 14399 0 0 0 28807 87 0 0 25 0 1 0 1855082179 56123392 13179 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 13702 13179 145 145 0 13557 0 [pid=3157] vsize: 54808 Current children cumulated CPU time (s) 288.94 Current children cumulated vsize (Kb) 56932 [startup+300.032 s] Raw data (loadavg): 0.99 0.69 0.31 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 14759 0 0 0 29801 91 0 0 25 0 1 0 1855082179 57581568 13539 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 14058 13539 145 145 0 13913 0 [pid=3157] vsize: 56232 Current children cumulated CPU time (s) 298.92 Current children cumulated vsize (Kb) 58356 [startup+310.032 s] Raw data (loadavg): 0.99 0.70 0.32 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 14964 0 0 0 30797 92 0 0 25 0 1 0 1855082179 58408960 13744 4294967295 134512640 135094434 3221224432 3221223024 134551740 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 14260 13744 145 145 0 14115 0 [pid=3157] vsize: 57040 Current children cumulated CPU time (s) 308.89 Current children cumulated vsize (Kb) 59164 [startup+320.033 s] Raw data (loadavg): 0.99 0.71 0.32 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15176 0 0 0 31793 94 0 0 25 0 1 0 1855082179 59265024 13956 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 14469 13956 145 145 0 14324 0 [pid=3157] vsize: 57876 Current children cumulated CPU time (s) 318.87 Current children cumulated vsize (Kb) 60000 [startup+330.034 s] Raw data (loadavg): 0.99 0.72 0.33 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15379 0 0 0 32790 95 0 0 25 0 1 0 1855082179 60100608 14159 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 14673 14159 145 145 0 14528 0 [pid=3157] vsize: 58692 Current children cumulated CPU time (s) 328.85 Current children cumulated vsize (Kb) 60816 [startup+340.034 s] Raw data (loadavg): 0.99 0.73 0.34 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15587 0 0 0 33787 96 0 0 25 0 1 0 1855082179 60940288 14367 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 14878 14367 145 145 0 14733 0 [pid=3157] vsize: 59512 Current children cumulated CPU time (s) 338.83 Current children cumulated vsize (Kb) 61636 [startup+350.035 s] Raw data (loadavg): 0.99 0.74 0.34 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15846 0 0 0 34782 99 0 0 25 0 1 0 1855082179 61980672 14626 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 15132 14626 145 145 0 14987 0 [pid=3157] vsize: 60528 Current children cumulated CPU time (s) 348.81 Current children cumulated vsize (Kb) 62652 [startup+360.036 s] Raw data (loadavg): 0.99 0.75 0.35 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16046 0 0 0 35779 100 0 0 25 0 1 0 1855082179 63307776 14826 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 15456 14826 145 145 0 15311 0 [pid=3157] vsize: 61824 Current children cumulated CPU time (s) 358.79 Current children cumulated vsize (Kb) 63948 [startup+370.037 s] Raw data (loadavg): 0.99 0.75 0.36 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16307 0 0 0 36774 102 0 0 25 0 1 0 1855082179 64364544 15087 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 15714 15087 145 145 0 15569 0 [pid=3157] vsize: 62856 Current children cumulated CPU time (s) 368.76 Current children cumulated vsize (Kb) 64980 [startup+380.037 s] Raw data (loadavg): 0.99 0.76 0.36 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16529 0 0 0 37770 104 0 0 25 0 1 0 1855082179 65261568 15309 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 15933 15309 145 145 0 15788 0 [pid=3157] vsize: 63732 Current children cumulated CPU time (s) 378.74 Current children cumulated vsize (Kb) 65856 [startup+390.039 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16703 0 0 0 38768 104 0 0 25 0 1 0 1855082179 65966080 15483 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 16105 15483 145 145 0 15960 0 [pid=3157] vsize: 64420 Current children cumulated CPU time (s) 388.72 Current children cumulated vsize (Kb) 66544 [startup+400.04 s] Raw data (loadavg): 0.99 0.78 0.38 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16888 0 0 0 39766 105 0 0 25 0 1 0 1855082179 66711552 15668 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 16287 15668 145 145 0 16142 0 [pid=3157] vsize: 65148 Current children cumulated CPU time (s) 398.71 Current children cumulated vsize (Kb) 67272 [startup+410.04 s] Raw data (loadavg): 0.99 0.78 0.38 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 17209 0 0 0 40760 107 0 0 25 0 1 0 1855082179 68005888 15989 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 16603 15989 145 145 0 16458 0 [pid=3157] vsize: 66412 Current children cumulated CPU time (s) 408.67 Current children cumulated vsize (Kb) 68536 [startup+420.041 s] Raw data (loadavg): 0.99 0.79 0.39 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 17623 0 0 0 41753 110 0 0 25 0 1 0 1855082179 69672960 16403 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 17010 16403 145 145 0 16865 0 [pid=3157] vsize: 68040 Current children cumulated CPU time (s) 418.63 Current children cumulated vsize (Kb) 70164 [startup+430.041 s] Raw data (loadavg): 0.99 0.80 0.39 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 18031 0 0 0 42746 113 0 0 25 0 1 0 1855082179 71315456 16811 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 17411 16811 145 145 0 17266 0 [pid=3157] vsize: 69644 Current children cumulated CPU time (s) 428.59 Current children cumulated vsize (Kb) 71768 [startup+440.042 s] Raw data (loadavg): 0.99 0.80 0.40 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 18463 0 0 0 43738 117 0 0 25 0 1 0 1855082179 73056256 17243 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 17836 17243 145 145 0 17691 0 [pid=3157] vsize: 71344 Current children cumulated CPU time (s) 438.55 Current children cumulated vsize (Kb) 73468 [startup+450.043 s] Raw data (loadavg): 0.99 0.81 0.40 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 18800 0 0 0 44729 120 0 0 25 0 1 0 1855082179 74412032 17580 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 18167 17580 145 145 0 18022 0 [pid=3157] vsize: 72668 Current children cumulated CPU time (s) 448.49 Current children cumulated vsize (Kb) 74792 [startup+460.044 s] Raw data (loadavg): 0.99 0.81 0.41 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 19154 0 0 0 45723 122 0 0 25 0 1 0 1855082179 75845632 17934 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 18517 17934 145 145 0 18372 0 [pid=3157] vsize: 74068 Current children cumulated CPU time (s) 458.45 Current children cumulated vsize (Kb) 76192 [startup+470.044 s] Raw data (loadavg): 0.99 0.82 0.42 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 19500 0 0 0 46717 125 0 0 25 0 1 0 1855082179 77242368 18280 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 18858 18280 145 145 0 18713 0 [pid=3157] vsize: 75432 Current children cumulated CPU time (s) 468.42 Current children cumulated vsize (Kb) 77556 [startup+480.045 s] Raw data (loadavg): 0.99 0.83 0.42 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 19827 0 0 0 47711 127 0 0 25 0 1 0 1855082179 78573568 18607 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 19183 18607 145 145 0 19038 0 [pid=3157] vsize: 76732 Current children cumulated CPU time (s) 478.38 Current children cumulated vsize (Kb) 78856 [startup+490.046 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 20137 0 0 0 48705 130 0 0 25 0 1 0 1855082179 79831040 18917 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 19490 18917 145 145 0 19345 0 [pid=3157] vsize: 77960 Current children cumulated CPU time (s) 488.35 Current children cumulated vsize (Kb) 80084 [startup+500.047 s] Raw data (loadavg): 0.99 0.84 0.43 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 20563 0 0 0 49697 132 0 0 25 0 1 0 1855082179 81551360 19343 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 19910 19343 145 145 0 19765 0 [pid=3157] vsize: 79640 Current children cumulated CPU time (s) 498.29 Current children cumulated vsize (Kb) 81764 [startup+510.047 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 21162 0 0 0 50687 136 0 0 25 0 1 0 1855082179 83972096 19942 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 20501 19942 145 145 0 20356 0 [pid=3157] vsize: 82004 Current children cumulated CPU time (s) 508.23 Current children cumulated vsize (Kb) 84128 [startup+520.048 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 21741 0 0 0 51678 139 0 0 25 0 1 0 1855082179 86310912 20521 4294967295 134512640 135094434 3221224432 3221223024 134556724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 21072 20521 145 145 0 20927 0 [pid=3157] vsize: 84288 Current children cumulated CPU time (s) 518.17 Current children cumulated vsize (Kb) 86412 [startup+530.049 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 22294 0 0 0 52668 143 0 0 25 0 1 0 1855082179 88547328 21074 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 21618 21074 145 145 0 21473 0 [pid=3157] vsize: 86472 Current children cumulated CPU time (s) 528.11 Current children cumulated vsize (Kb) 88596 [startup+540.05 s] Raw data (loadavg): 0.99 0.85 0.46 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 22839 0 0 0 53658 147 0 0 25 0 1 0 1855082179 90746880 21619 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 22155 21619 145 145 0 22010 0 [pid=3157] vsize: 88620 Current children cumulated CPU time (s) 538.05 Current children cumulated vsize (Kb) 90744 [startup+550.05 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 23272 0 0 0 54650 150 0 0 25 0 1 0 1855082179 92499968 22052 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 22583 22052 145 145 0 22438 0 [pid=3157] vsize: 90332 Current children cumulated CPU time (s) 548 Current children cumulated vsize (Kb) 92456 [startup+560.05 s] Raw data (loadavg): 0.99 0.86 0.47 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 23636 0 0 0 55645 153 0 0 25 0 1 0 1855082179 93974528 22416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 22943 22416 145 145 0 22798 0 [pid=3157] vsize: 91772 Current children cumulated CPU time (s) 557.98 Current children cumulated vsize (Kb) 93896 [startup+570.052 s] Raw data (loadavg): 0.99 0.87 0.47 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 23998 0 0 0 56637 155 0 0 25 0 1 0 1855082179 95444992 22778 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 23302 22778 145 145 0 23157 0 [pid=3157] vsize: 93208 Current children cumulated CPU time (s) 567.92 Current children cumulated vsize (Kb) 95332 [startup+580.053 s] Raw data (loadavg): 0.99 0.87 0.48 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 24314 0 0 0 57632 158 0 0 25 0 1 0 1855082179 96722944 23094 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 23614 23094 145 145 0 23469 0 [pid=3157] vsize: 94456 Current children cumulated CPU time (s) 577.9 Current children cumulated vsize (Kb) 96580 [startup+590.054 s] Raw data (loadavg): 0.99 0.87 0.48 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 24623 0 0 0 58627 160 0 0 25 0 1 0 1855082179 97988608 23403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 23923 23403 145 145 0 23778 0 [pid=3157] vsize: 95692 Current children cumulated CPU time (s) 587.87 Current children cumulated vsize (Kb) 97816 [startup+600.055 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 24924 0 0 0 59621 162 0 0 25 0 1 0 1855082179 99213312 23704 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 24222 23704 145 145 0 24077 0 [pid=3157] vsize: 96888 Current children cumulated CPU time (s) 597.83 Current children cumulated vsize (Kb) 99012 [startup+610.055 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25211 0 0 0 60617 164 0 0 25 0 1 0 1855082179 101433344 23991 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 24764 23991 145 145 0 24619 0 [pid=3157] vsize: 99056 Current children cumulated CPU time (s) 607.81 Current children cumulated vsize (Kb) 101180 [startup+620.056 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25482 0 0 0 61612 167 0 0 25 0 1 0 1855082179 102543360 24262 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 25035 24262 145 145 0 24890 0 [pid=3157] vsize: 100140 Current children cumulated CPU time (s) 617.79 Current children cumulated vsize (Kb) 102264 [startup+630.057 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25713 0 0 0 62608 169 0 0 25 0 1 0 1855082179 103473152 24493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 25262 24493 145 145 0 25117 0 [pid=3157] vsize: 101048 Current children cumulated CPU time (s) 627.77 Current children cumulated vsize (Kb) 103172 [startup+640.058 s] Raw data (loadavg): 0.99 0.89 0.51 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25951 0 0 0 63605 170 0 0 25 0 1 0 1855082179 104464384 24731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 25504 24731 145 145 0 25359 0 [pid=3157] vsize: 102016 Current children cumulated CPU time (s) 637.75 Current children cumulated vsize (Kb) 104140 [startup+650.059 s] Raw data (loadavg): 0.99 0.89 0.51 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 26183 0 0 0 64601 172 0 0 25 0 1 0 1855082179 105422848 24963 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 25738 24963 145 145 0 25593 0 [pid=3157] vsize: 102952 Current children cumulated CPU time (s) 647.73 Current children cumulated vsize (Kb) 105076 [startup+660.06 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 26424 0 0 0 65597 175 0 0 25 0 1 0 1855082179 106397696 25204 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 25976 25204 145 145 0 25831 0 [pid=3157] vsize: 103904 Current children cumulated CPU time (s) 657.72 Current children cumulated vsize (Kb) 106028 [startup+670.061 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 26749 0 0 0 66593 177 0 0 25 0 1 0 1855082179 107732992 25529 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 26302 25529 145 145 0 26157 0 [pid=3157] vsize: 105208 Current children cumulated CPU time (s) 667.7 Current children cumulated vsize (Kb) 107332 [startup+680.062 s] Raw data (loadavg): 0.99 0.90 0.53 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27033 0 0 0 67589 178 0 0 25 0 1 0 1855082179 108883968 25813 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 26583 25813 145 145 0 26438 0 [pid=3157] vsize: 106332 Current children cumulated CPU time (s) 677.67 Current children cumulated vsize (Kb) 108456 [startup+690.063 s] Raw data (loadavg): 0.99 0.91 0.53 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27329 0 0 0 68585 180 0 0 25 0 1 0 1855082179 110084096 26109 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 26876 26109 145 145 0 26731 0 [pid=3157] vsize: 107504 Current children cumulated CPU time (s) 687.65 Current children cumulated vsize (Kb) 109628 [startup+700.064 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27615 0 0 0 69580 182 0 0 25 0 1 0 1855082179 111251456 26395 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 27161 26395 145 145 0 27016 0 [pid=3157] vsize: 108644 Current children cumulated CPU time (s) 697.62 Current children cumulated vsize (Kb) 110768 [startup+710.065 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27895 0 0 0 70576 184 0 0 25 0 1 0 1855082179 112386048 26675 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 27438 26675 145 145 0 27293 0 [pid=3157] vsize: 109752 Current children cumulated CPU time (s) 707.6 Current children cumulated vsize (Kb) 111876 [startup+720.066 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28167 0 0 0 71570 186 0 0 25 0 1 0 1855082179 113504256 26947 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 27711 26947 145 145 0 27566 0 [pid=3157] vsize: 110844 Current children cumulated CPU time (s) 717.56 Current children cumulated vsize (Kb) 112968 [startup+730.067 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28397 0 0 0 72565 188 0 0 25 0 1 0 1855082179 114450432 27177 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 27942 27177 145 145 0 27797 0 [pid=3157] vsize: 111768 Current children cumulated CPU time (s) 727.53 Current children cumulated vsize (Kb) 113892 [startup+740.067 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28645 0 0 0 73560 191 0 0 25 0 1 0 1855082179 115445760 27425 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 28185 27425 145 145 0 28040 0 [pid=3157] vsize: 112740 Current children cumulated CPU time (s) 737.51 Current children cumulated vsize (Kb) 114864 [startup+750.068 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28882 0 0 0 74556 193 0 0 25 0 1 0 1855082179 116416512 27662 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 28422 27662 145 145 0 28277 0 [pid=3157] vsize: 113688 Current children cumulated CPU time (s) 747.49 Current children cumulated vsize (Kb) 115812 [startup+760.068 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29099 0 0 0 75553 194 0 0 25 0 1 0 1855082179 117309440 27879 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 28640 27879 145 145 0 28495 0 [pid=3157] vsize: 114560 Current children cumulated CPU time (s) 757.47 Current children cumulated vsize (Kb) 116684 [startup+770.069 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29299 0 0 0 76550 195 0 0 25 0 1 0 1855082179 118112256 28079 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 28836 28079 145 145 0 28691 0 [pid=3157] vsize: 115344 Current children cumulated CPU time (s) 767.45 Current children cumulated vsize (Kb) 117468 [startup+780.069 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29490 0 0 0 77547 196 0 0 25 0 1 0 1855082179 118898688 28270 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 29028 28270 145 145 0 28883 0 [pid=3157] vsize: 116112 Current children cumulated CPU time (s) 777.43 Current children cumulated vsize (Kb) 118236 [startup+790.069 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29648 0 0 0 78546 197 0 0 25 0 1 0 1855082179 119545856 28428 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 29186 28428 145 145 0 29041 0 [pid=3157] vsize: 116744 Current children cumulated CPU time (s) 787.43 Current children cumulated vsize (Kb) 118868 [startup+800.07 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29819 0 0 0 79543 198 0 0 25 0 1 0 1855082179 120246272 28599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 29357 28599 145 145 0 29212 0 [pid=3157] vsize: 117428 Current children cumulated CPU time (s) 797.41 Current children cumulated vsize (Kb) 119552 [startup+810.071 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30030 0 0 0 80540 199 0 0 25 0 1 0 1855082179 121098240 28810 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 29565 28810 145 145 0 29420 0 [pid=3157] vsize: 118260 Current children cumulated CPU time (s) 807.39 Current children cumulated vsize (Kb) 120384 [startup+820.072 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30214 0 0 0 81537 200 0 0 25 0 1 0 1855082179 121835520 28994 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 29745 28994 145 145 0 29600 0 [pid=3157] vsize: 118980 Current children cumulated CPU time (s) 817.37 Current children cumulated vsize (Kb) 121104 [startup+830.072 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30381 0 0 0 82533 202 0 0 25 0 1 0 1855082179 122515456 29161 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 29911 29161 145 145 0 29766 0 [pid=3157] vsize: 119644 Current children cumulated CPU time (s) 827.35 Current children cumulated vsize (Kb) 121768 [startup+840.073 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30556 0 0 0 83532 203 0 0 25 0 1 0 1855082179 123219968 29336 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 30083 29336 145 145 0 29938 0 [pid=3157] vsize: 120332 Current children cumulated CPU time (s) 837.35 Current children cumulated vsize (Kb) 122456 [startup+850.074 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30725 0 0 0 84529 203 0 0 25 0 1 0 1855082179 123899904 29505 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 30249 29505 145 145 0 30104 0 [pid=3157] vsize: 120996 Current children cumulated CPU time (s) 847.32 Current children cumulated vsize (Kb) 123120 [startup+860.074 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30879 0 0 0 85526 205 0 0 25 0 1 0 1855082179 124522496 29659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 30401 29659 145 145 0 30256 0 [pid=3157] vsize: 121604 Current children cumulated CPU time (s) 857.31 Current children cumulated vsize (Kb) 123728 [startup+870.075 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31038 0 0 0 86523 206 0 0 25 0 1 0 1855082179 125194240 29818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 30565 29818 145 145 0 30420 0 [pid=3157] vsize: 122260 Current children cumulated CPU time (s) 867.29 Current children cumulated vsize (Kb) 124384 [startup+880.076 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31193 0 0 0 87521 207 0 0 25 0 1 0 1855082179 125812736 29973 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 30716 29973 145 145 0 30571 0 [pid=3157] vsize: 122864 Current children cumulated CPU time (s) 877.28 Current children cumulated vsize (Kb) 124988 [startup+890.076 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31343 0 0 0 88518 208 0 0 25 0 1 0 1855082179 126414848 30123 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 30863 30123 145 145 0 30718 0 [pid=3157] vsize: 123452 Current children cumulated CPU time (s) 887.26 Current children cumulated vsize (Kb) 125576 [startup+900.077 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31490 0 0 0 89516 209 0 0 25 0 1 0 1855082179 127025152 30270 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 31012 30270 145 145 0 30867 0 [pid=3157] vsize: 124048 Current children cumulated CPU time (s) 897.25 Current children cumulated vsize (Kb) 126172 [startup+910.077 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31641 0 0 0 90512 211 0 0 25 0 1 0 1855082179 127635456 30421 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 31161 30421 145 145 0 31016 0 [pid=3157] vsize: 124644 Current children cumulated CPU time (s) 907.23 Current children cumulated vsize (Kb) 126768 [startup+920.077 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31789 0 0 0 91510 212 0 0 25 0 1 0 1855082179 128241664 30569 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 31309 30569 145 145 0 31164 0 [pid=3157] vsize: 125236 Current children cumulated CPU time (s) 917.22 Current children cumulated vsize (Kb) 127360 [startup+930.078 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31928 0 0 0 92508 213 0 0 25 0 1 0 1855082179 128802816 30708 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 31446 30708 145 145 0 31301 0 [pid=3157] vsize: 125784 Current children cumulated CPU time (s) 927.21 Current children cumulated vsize (Kb) 127908 [startup+940.078 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32070 0 0 0 93505 214 0 0 25 0 1 0 1855082179 129372160 30850 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 31585 30850 145 145 0 31440 0 [pid=3157] vsize: 126340 Current children cumulated CPU time (s) 937.19 Current children cumulated vsize (Kb) 128464 [startup+950.079 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32223 0 0 0 94503 215 0 0 25 0 1 0 1855082179 129994752 31003 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 31737 31003 145 145 0 31592 0 [pid=3157] vsize: 126948 Current children cumulated CPU time (s) 947.18 Current children cumulated vsize (Kb) 129072 [startup+960.08 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32360 0 0 0 95500 216 0 0 25 0 1 0 1855082179 130547712 31140 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 31872 31140 145 145 0 31727 0 [pid=3157] vsize: 127488 Current children cumulated CPU time (s) 957.16 Current children cumulated vsize (Kb) 129612 [startup+970.08 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32506 0 0 0 96498 217 0 0 25 0 1 0 1855082179 131158016 31286 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 32021 31286 145 145 0 31876 0 [pid=3157] vsize: 128084 Current children cumulated CPU time (s) 967.15 Current children cumulated vsize (Kb) 130208 [startup+980.081 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32643 0 0 0 97495 218 0 0 25 0 1 0 1855082179 131710976 31423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3157/statm): 32156 31423 145 145 0 32011 0 [pid=3157] vsize: 128624 Current children cumulated CPU time (s) 977.13 Current children cumulated vsize (Kb) 130748 [startup+990.082 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32803 0 0 0 98491 220 0 0 25 0 1 0 1855082179 132407296 31583 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 32326 31583 145 145 0 32181 0 [pid=3157] vsize: 129304 Current children cumulated CPU time (s) 987.11 Current children cumulated vsize (Kb) 131428 [startup+1000.08 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32931 0 0 0 99489 221 0 0 25 0 1 0 1855082179 132947968 31711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 32458 31711 145 145 0 32313 0 [pid=3157] vsize: 129832 Current children cumulated CPU time (s) 997.1 Current children cumulated vsize (Kb) 131956 [startup+1010.08 s] Raw data (loadavg): 0.99 0.96 0.65 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33051 0 0 0 100487 222 0 0 25 0 1 0 1855082179 133431296 31831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 32576 31831 145 145 0 32431 0 [pid=3157] vsize: 130304 Current children cumulated CPU time (s) 1007.09 Current children cumulated vsize (Kb) 132428 [startup+1020.09 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33190 0 0 0 101485 223 0 0 25 0 1 0 1855082179 134021120 31970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 32720 31970 145 145 0 32575 0 [pid=3157] vsize: 130880 Current children cumulated CPU time (s) 1017.08 Current children cumulated vsize (Kb) 133004 [startup+1030.09 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33318 0 0 0 102483 223 0 0 25 0 1 0 1855082179 134529024 32098 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 32844 32098 145 145 0 32699 0 [pid=3157] vsize: 131376 Current children cumulated CPU time (s) 1027.06 Current children cumulated vsize (Kb) 133500 [startup+1040.09 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33442 0 0 0 103481 224 0 0 25 0 1 0 1855082179 135049216 32222 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 32971 32222 145 145 0 32826 0 [pid=3157] vsize: 131884 Current children cumulated CPU time (s) 1037.05 Current children cumulated vsize (Kb) 134008 [startup+1050.09 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33581 0 0 0 104478 226 0 0 25 0 1 0 1855082179 135606272 32361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33107 32361 145 145 0 32962 0 [pid=3157] vsize: 132428 Current children cumulated CPU time (s) 1047.04 Current children cumulated vsize (Kb) 134552 [startup+1060.09 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33717 0 0 0 105477 227 0 0 25 0 1 0 1855082179 136159232 32497 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33242 32497 145 145 0 33097 0 [pid=3157] vsize: 132968 Current children cumulated CPU time (s) 1057.04 Current children cumulated vsize (Kb) 135092 [startup+1070.09 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33857 0 0 0 106476 227 0 0 25 0 1 0 1855082179 136757248 32637 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33388 32637 145 145 0 33243 0 [pid=3157] vsize: 133552 Current children cumulated CPU time (s) 1067.03 Current children cumulated vsize (Kb) 135676 [startup+1080.09 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33980 0 0 0 107475 228 0 0 25 0 1 0 1855082179 137248768 32760 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33508 32760 145 145 0 33363 0 [pid=3157] vsize: 134032 Current children cumulated CPU time (s) 1077.03 Current children cumulated vsize (Kb) 136156 [startup+1090.09 s] Raw data (loadavg): 0.99 0.96 0.68 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34108 0 0 0 108473 228 0 0 25 0 1 0 1855082179 137809920 32888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33645 32888 145 145 0 33500 0 [pid=3157] vsize: 134580 Current children cumulated CPU time (s) 1087.01 Current children cumulated vsize (Kb) 136704 [startup+1100.09 s] Raw data (loadavg): 0.99 0.96 0.68 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34214 0 0 0 109471 229 0 0 25 0 1 0 1855082179 138235904 32994 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33749 32994 145 145 0 33604 0 [pid=3157] vsize: 134996 Current children cumulated CPU time (s) 1097 Current children cumulated vsize (Kb) 137120 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.68 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34316 0 0 0 110470 230 0 0 25 0 1 0 1855082179 138641408 33096 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33848 33096 145 145 0 33703 0 [pid=3157] vsize: 135392 Current children cumulated CPU time (s) 1107 Current children cumulated vsize (Kb) 137516 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34440 0 0 0 111468 231 0 0 25 0 1 0 1855082179 139145216 33220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 33971 33220 145 145 0 33826 0 [pid=3157] vsize: 135884 Current children cumulated CPU time (s) 1116.99 Current children cumulated vsize (Kb) 138008 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34575 0 0 0 112466 232 0 0 25 0 1 0 1855082179 139681792 33355 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34102 33355 145 145 0 33957 0 [pid=3157] vsize: 136408 Current children cumulated CPU time (s) 1126.98 Current children cumulated vsize (Kb) 138532 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34699 0 0 0 113465 233 0 0 25 0 1 0 1855082179 140185600 33479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34225 33479 145 145 0 34080 0 [pid=3157] vsize: 136900 Current children cumulated CPU time (s) 1136.98 Current children cumulated vsize (Kb) 139024 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34823 0 0 0 114463 234 0 0 25 0 1 0 1855082179 140697600 33603 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34350 33603 145 145 0 34205 0 [pid=3157] vsize: 137400 Current children cumulated CPU time (s) 1146.97 Current children cumulated vsize (Kb) 139524 [startup+1160.1 s] Raw data (loadavg): 1.15 1.00 0.71 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34944 0 0 0 115461 235 0 0 25 0 1 0 1855082179 141201408 33724 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34473 33724 145 145 0 34328 0 [pid=3157] vsize: 137892 Current children cumulated CPU time (s) 1156.96 Current children cumulated vsize (Kb) 140016 [startup+1170.1 s] Raw data (loadavg): 1.13 1.00 0.71 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35072 0 0 0 116458 237 0 0 25 0 1 0 1855082179 141717504 33852 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34599 33852 145 145 0 34454 0 [pid=3157] vsize: 138396 Current children cumulated CPU time (s) 1166.95 Current children cumulated vsize (Kb) 140520 [startup+1180.1 s] Raw data (loadavg): 1.11 1.00 0.71 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35195 0 0 0 117456 238 0 0 25 0 1 0 1855082179 142217216 33975 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34721 33975 145 145 0 34576 0 [pid=3157] vsize: 138884 Current children cumulated CPU time (s) 1176.94 Current children cumulated vsize (Kb) 141008 [startup+1190.1 s] Raw data (loadavg): 1.09 1.00 0.72 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35316 0 0 0 118455 238 0 0 25 0 1 0 1855082179 142708736 34096 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34841 34096 145 145 0 34696 0 [pid=3157] vsize: 139364 Current children cumulated CPU time (s) 1186.93 Current children cumulated vsize (Kb) 141488 [startup+1200.1 s] Raw data (loadavg): 1.08 1.00 0.72 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35439 0 0 0 119453 239 0 0 25 0 1 0 1855082179 143224832 34219 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 34967 34219 145 145 0 34822 0 [pid=3157] vsize: 139868 Current children cumulated CPU time (s) 1196.92 Current children cumulated vsize (Kb) 141992 [startup+1210.1 s] Raw data (loadavg): 1.07 1.00 0.72 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35572 0 0 0 120451 239 0 0 25 0 1 0 1855082179 143740928 34352 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 35093 34352 145 145 0 34948 0 [pid=3157] vsize: 140372 Current children cumulated CPU time (s) 1206.9 Current children cumulated vsize (Kb) 142496 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.07 1.00 0.72 2/57 3157 Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3153/statm): 531 226 485 147 0 384 0 [pid=3153] vsize: 2124 Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35572 0 0 0 120451 239 0 0 25 0 1 0 1855082179 143740928 34352 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3157/statm): 35093 34352 145 145 0 34948 0 [pid=3157] vsize: 140372 Current children cumulated CPU time (s) 1206.9 Current children cumulated vsize (Kb) 142496 Sending SIGTERM to -3153 Sleeping 2 seconds One traced child (pid=3153) ended because it received signal 15 (SIGTERM) One traced child (pid=3157) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1206.98 CPU user time (s): 1204.52 CPU system time (s): 2.46362 CPU usage (%): 99.7368 Max. virtual memory (cumulated for all children) (Kb): 142496
ERROR: no interpretation found !