Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-blend.opb |
MD5SUM | 7713e9174526352f04e3c528ca3ecb01 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 440 |
Biggest coefficient in the objective function | 14050918400 |
Number of bits for the biggest coefficient in the objective function | 34 |
Sum of the numbers in the objective function | 198838131525 |
Number of bits of the sum of numbers in the objective function | 38 |
Biggest number in a constraint | 76598476800 |
Number of bits of the biggest number in a constraint | 37 |
Biggest sum of numbers in a constraint | 770522270100 |
Number of bits of the biggest sum of numbers | 40 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1238.79 |
Number of variables | 1660 |
Total number of constraints | 74 |
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 | 74 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 520 |
LAUNCH ON wulflinc12 THE 2005-09-20 02:30:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3139 boxname=wulflinc12 idbench=795 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 7713e9174526352f04e3c528ca3ecb01 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-blend.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-blend.opb IDLAUNCH: 3139 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 914080 kB Buffers: 33176 kB Cached: 56704 kB SwapCached: 492 kB Active: 39388 kB Inactive: 53000 kB HighTotal: 131008 kB HighFree: 72156 kB LowTotal: 903652 kB LowFree: 841924 kB SwapTotal: 2097136 kB SwapFree: 2096072 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5884 kB Slab: 22376 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 02:51:03 (client local time) WITH STATUS 0 IN 1208.28 SECONDS stats: 3139 7 1208.28 0
c Parsing PB file... c Converting 109 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ####################################### c -- Clauses(.)/Splits(s): (none) c ---[ 107]---> BDD-cost: 22 c ---[ 105]---> Sorter-cost: 7788 Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 7489 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Adder-cost: 527 maxlim: 122860000 bits: 28/27 c ---[ 99]---> Adder-cost: 1024 maxlim: 20972465200 bits: 35/35 c ---[ 97]---> BDD-cost: 96 c ---[ 95]---> BDD-cost: 91 c ---[ 93]---> BDD-cost: 91 c ---[ 91]---> BDD-cost: 60 c ---[ 89]---> BDD-cost: 181 c ---[ 87]---> BDD-cost: 96 c ---[ 85]---> BDD-cost: 43 c ---[ 83]---> Sorter-cost: 5756 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 c ---[ 81]---> Sorter-cost: 5836 Base: 5 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2 c ---[ 79]---> Adder-cost: 581 maxlim: 3069000 bits: 22/22 c ---[ 77]---> Adder-cost: 394 maxlim: 3265678 bits: 22/22 c ---[ 75]---> BDD-cost: 23 c ---[ 73]---> Adder-cost: 714 maxlim: 30705000 bits: 26/25 c ---[ 71]---> Adder-cost: 646 maxlim: 12790000 bits: 25/24 c ---[ 69]---> Adder-cost: 374 maxlim: 2046000 bits: 22/21 c ---[ 67]---> BDD-cost: 19 c ---[ 65]---> Sorter-cost: 1384 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> Sorter-cost: 1189 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> BDD-cost: 83 c ---[ 59]---> Sorter-cost: 826 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 1189 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> BDD-cost: 130 c ---[ 53]---> BDD-cost: 106 c ---[ 51]---> Adder-cost: 1024 maxlim: 88981655 bits: 27/27 c ---[ 49]---> BDD-cost: 212 c ---[ 47]---> Adder-cost: 1428 maxlim: 104868276002 bits: 38/37 c ---[ 45]---> Adder-cost: 2947 maxlim: 25381871133 bits: 36/35 c ---[ 43]---> Adder-cost: 1579 maxlim: 8620523 bits: 25/24 c ---[ 41]---> Adder-cost: 2410 maxlim: 464776490 bits: 30/29 c ---[ 40]---> Adder-cost: 1260 maxlim: 328653009 bits: 29/29 c ---[ 39]---> Adder-cost: 1094 maxlim: 65730601 bits: 27/26 c ---[ 38]---> Sorter-cost: 3239 Base: 2 2 2 3 2 2 2 2 2 2 2 5 c ---[ 37]---> Adder-cost: 426 maxlim: 1216936 bits: 21/21 c ---[ 36]---> Sorter-cost:10135 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost:10046 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Adder-cost: 510 maxlim: 25570000 bits: 25/25 c ---[ 32]---> Adder-cost: 1084 maxlim: 63240309 bits: 27/26 c ---[ 31]---> Adder-cost: 1020 maxlim: 158100774 bits: 28/28 c ---[ 30]---> Sorter-cost: 2940 Base: 2 2 2 2 3 2 2 2 2 2 2 5 c ---[ 29]---> Adder-cost: 390 maxlim: 1216301 bits: 21/21 c ---[ 28]---> Sorter-cost: 8062 Base: 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 8547 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Adder-cost: 1314 maxlim: 593082699 bits: 30/30 c ---[ 25]---> Adder-cost: 1214 maxlim: 593082699 bits: 30/30 c ---[ 24]---> Sorter-cost: 2940 Base: 2 2 2 2 3 2 2 2 2 2 2 5 c ---[ 23]---> Adder-cost: 390 maxlim: 1216301 bits: 21/21 c ---[ 21]---> Sorter-cost: 5137 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 8062 Base: 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 c ---[ 19]---> Sorter-cost: 8547 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 18]---> Sorter-cost: 7118 Base: 2 2 2 5 2 2 2 2 2 2 2 2 2 5 2 5 c ---[ 17]---> Sorter-cost: 930 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 16]---> Sorter-cost: 1542 Base: 2 2 2 2 2 2 2 2 2 5 3 2 2 2 c ---[ 15]---> Sorter-cost: 1628 Base: 2 2 2 2 2 2 2 2 2 c ---[ 14]---> Sorter-cost: 198 Base: 2 2 2 2 2 2 2 2 c ---[ 13]---> BDD-cost: 9 c ---[ 12]---> BDD-cost: 11 c ---[ 11]---> Sorter-cost: 609 Base: 2 2 2 2 2 2 2 2 5 2 2 c ---[ 9]---> BDD-cost: 63 c ---[ 8]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 363 Base: 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 817 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 2511 Base: 2 2 2 2 2 2 2 2 2 2 2 13 2 2 c ---[ 2]---> Sorter-cost: 543 Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 0]---> Adder-cost: 680 maxlim: 10220000 bits: 24/24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 282586 801955 | 94195 0 0 nan | 0.000 % | c | 102 | 186139 546043 | 103614 75 482 6.4 | 58.903 % | c | 252 | 186111 545965 | 113975 222 1697 7.6 | 58.910 % | c | 477 | 185719 544917 | 125373 427 4109 9.6 | 58.989 % | c | 814 | 185514 544451 | 137910 756 8950 11.8 | 59.036 % | c | 1321 | 185226 543783 | 151701 1252 16143 12.9 | 59.112 % | c | 2083 | 178368 526964 | 166872 1996 33259 16.7 | 60.770 % | c | 3222 | 176691 522313 | 183559 3049 61458 20.2 | 61.065 % | c | 4931 | 176350 521492 | 201915 4703 99890 21.2 | 61.155 % | c | 7497 | 160029 474147 | 222106 6408 119962 18.7 | 64.726 % | c | 11341 | 155019 460400 | 244317 9968 192862 19.3 | 65.817 % | c | 17107 | 151546 451557 | 268749 15208 374307 24.6 | 66.639 % | c | 25756 | 142542 421838 | 295624 23544 659302 28.0 | 68.353 % | c | 38730 | 26878 91344 | 325186 30331 955207 31.5 | 94.816 % | c | 58191 | 24219 82020 | 357705 48647 1682017 34.6 | 95.228 % | c | 87384 | 24216 82012 | 393475 77839 3607275 46.3 | 95.229 % | c | 131175 | 24157 81813 | 432823 121622 5877976 48.3 | 95.237 % | c | 196861 | 24151 81797 | 476105 187306 9962669 53.2 | 95.238 % |
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/10227/stat): 10227 (minisat+_script) R 10226 10227 8263 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796713066 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/10227/statm): 174 3 169 147 0 27 0 [pid=10227] 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=10228 New process pid=10229 New process pid=10230 execve syscall for /bin/sed executable One traced child (pid=10229) 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=10230) exited with status: 0 One traced child (pid=10228) exited with status: 0 New process pid=10231 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-blend.opb [startup+10.0034 s] Raw data (loadavg): 0.79 0.91 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 3084 0 0 0 974 12 0 0 25 0 1 0 1796713070 6369280 1460 4294967295 134512640 135094434 3221224432 3221221808 134600301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10231/statm): 1555 1460 145 145 0 1410 0 [pid=10231] vsize: 6220 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 8344 [startup+20.0042 s] Raw data (loadavg): 0.82 0.91 0.97 1/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) T 10227 10227 8263 0 -1 0 4636 0 0 0 1968 16 0 0 25 0 1 0 1796713070 9867264 2310 4294967295 134512640 135094434 3221224432 3221213884 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2409 2310 145 145 0 2264 0 [pid=10231] vsize: 9636 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 11760 [startup+30.0051 s] Raw data (loadavg): 0.85 0.92 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 4744 0 0 0 2967 17 0 0 25 0 1 0 1796713070 6840320 1503 4294967295 134512640 135094434 3221224432 3221221784 134676989 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1670 1503 145 145 0 1525 0 [pid=10231] vsize: 6680 Current children cumulated CPU time (s) 29.85 Current children cumulated vsize (Kb) 8804 [startup+40.0059 s] Raw data (loadavg): 0.87 0.92 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 4753 0 0 0 3967 17 0 0 25 0 1 0 1796713070 6840320 1512 4294967295 134512640 135094434 3221224432 3221221980 134600233 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1670 1512 145 145 0 1525 0 [pid=10231] vsize: 6680 Current children cumulated CPU time (s) 39.85 Current children cumulated vsize (Kb) 8804 [startup+50.0077 s] Raw data (loadavg): 0.89 0.92 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 4967 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221218992 134677330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 49.86 Current children cumulated vsize (Kb) 8828 [startup+60.0086 s] Raw data (loadavg): 0.91 0.92 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 5967 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221219600 134676328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 59.86 Current children cumulated vsize (Kb) 8828 [startup+70.0094 s] Raw data (loadavg): 0.92 0.92 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 6967 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221220380 134676382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 69.86 Current children cumulated vsize (Kb) 8828 [startup+80.0102 s] Raw data (loadavg): 0.93 0.93 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 7967 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221220832 134677078 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 79.86 Current children cumulated vsize (Kb) 8828 [startup+90.0111 s] Raw data (loadavg): 0.94 0.93 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 8967 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221221000 134677084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 89.86 Current children cumulated vsize (Kb) 8828 [startup+100.012 s] Raw data (loadavg): 0.95 0.93 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 9967 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 99.86 Current children cumulated vsize (Kb) 8828 [startup+110.013 s] Raw data (loadavg): 0.96 0.93 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 10968 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 109.87 Current children cumulated vsize (Kb) 8828 [startup+120.014 s] Raw data (loadavg): 0.96 0.93 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 11968 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 119.87 Current children cumulated vsize (Kb) 8828 [startup+130.014 s] Raw data (loadavg): 0.97 0.94 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5302 0 0 0 12968 18 0 0 25 0 1 0 1796713070 6864896 1566 4294967295 134512640 135094434 3221224432 3221219968 134677035 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1676 1566 145 145 0 1531 0 [pid=10231] vsize: 6704 Current children cumulated CPU time (s) 129.87 Current children cumulated vsize (Kb) 8828 [startup+140.015 s] Raw data (loadavg): 0.97 0.94 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 5361 0 0 0 13968 18 0 0 25 0 1 0 1796713070 7651328 1625 4294967295 134512640 135094434 3221224432 3221221456 134677346 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1868 1625 145 145 0 1723 0 [pid=10231] vsize: 7472 Current children cumulated CPU time (s) 139.87 Current children cumulated vsize (Kb) 9596 [startup+150.016 s] Raw data (loadavg): 0.98 0.94 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 14960 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221220224 134677248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 149.85 Current children cumulated vsize (Kb) 9588 [startup+160.017 s] Raw data (loadavg): 0.98 0.94 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 15960 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 159.85 Current children cumulated vsize (Kb) 9588 [startup+170.018 s] Raw data (loadavg): 0.98 0.94 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 16960 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221104 134600186 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 169.85 Current children cumulated vsize (Kb) 9588 [startup+180.019 s] Raw data (loadavg): 0.98 0.94 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 17961 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221220400 134677323 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 179.86 Current children cumulated vsize (Kb) 9588 [startup+190.019 s] Raw data (loadavg): 0.99 0.94 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 18961 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 189.86 Current children cumulated vsize (Kb) 9588 [startup+200.02 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 19961 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221104 134600228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 199.86 Current children cumulated vsize (Kb) 9588 [startup+210.021 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 20961 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221200 134676311 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 209.86 Current children cumulated vsize (Kb) 9588 [startup+220.022 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 21961 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 219.86 Current children cumulated vsize (Kb) 9588 [startup+230.023 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 22962 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221280 134677330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 229.87 Current children cumulated vsize (Kb) 9588 [startup+240.024 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 23962 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221352 134677084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 239.87 Current children cumulated vsize (Kb) 9588 [startup+250.025 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 24962 24 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221220724 134676992 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 249.87 Current children cumulated vsize (Kb) 9588 [startup+260.026 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 25962 25 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221220732 134676382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 259.88 Current children cumulated vsize (Kb) 9588 [startup+270.027 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 26962 25 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221904 134677059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 269.88 Current children cumulated vsize (Kb) 9588 [startup+280.028 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 27963 25 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221456 134677340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 279.89 Current children cumulated vsize (Kb) 9588 [startup+290.028 s] Raw data (loadavg): 0.99 0.95 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 28963 25 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221220988 134677228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 289.89 Current children cumulated vsize (Kb) 9588 [startup+300.029 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 29963 25 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221632 134676589 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 299.89 Current children cumulated vsize (Kb) 9588 [startup+310.03 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7089 0 0 0 30963 25 0 0 25 0 1 0 1796713070 7643136 1623 4294967295 134512640 135094434 3221224432 3221221084 134676240 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1623 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 309.89 Current children cumulated vsize (Kb) 9588 [startup+320.03 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7096 0 0 0 31964 25 0 0 25 0 1 0 1796713070 7643136 1630 4294967295 134512640 135094434 3221224432 3221220928 134600228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1630 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 319.9 Current children cumulated vsize (Kb) 9588 [startup+330.031 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7096 0 0 0 32963 25 0 0 25 0 1 0 1796713070 7643136 1630 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1630 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 329.89 Current children cumulated vsize (Kb) 9588 [startup+340.032 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7096 0 0 0 33964 25 0 0 25 0 1 0 1796713070 7643136 1630 4294967295 134512640 135094434 3221224432 3221221156 134676608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1630 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 339.9 Current children cumulated vsize (Kb) 9588 [startup+350.033 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7096 0 0 0 34964 25 0 0 25 0 1 0 1796713070 7643136 1630 4294967295 134512640 135094434 3221224432 3221221620 134600673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1630 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 349.9 Current children cumulated vsize (Kb) 9588 [startup+360.034 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7096 0 0 0 35964 25 0 0 25 0 1 0 1796713070 7643136 1630 4294967295 134512640 135094434 3221224432 3221221616 134600241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1630 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 359.9 Current children cumulated vsize (Kb) 9588 [startup+370.034 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7108 0 0 0 36964 25 0 0 25 0 1 0 1796713070 7643136 1642 4294967295 134512640 135094434 3221224432 3221222144 134600162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 1866 1642 145 145 0 1721 0 [pid=10231] vsize: 7464 Current children cumulated CPU time (s) 369.9 Current children cumulated vsize (Kb) 9588 [startup+380.035 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7459 0 0 0 37964 26 0 0 25 0 1 0 1796713070 8994816 1993 4294967295 134512640 135094434 3221224432 3221221280 134676589 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 1993 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 379.91 Current children cumulated vsize (Kb) 10908 [startup+390.036 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7459 0 0 0 38964 26 0 0 25 0 1 0 1796713070 8994816 1993 4294967295 134512640 135094434 3221224432 3221221728 134677028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 1993 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 389.91 Current children cumulated vsize (Kb) 10908 [startup+400.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7459 0 0 0 39964 26 0 0 25 0 1 0 1796713070 8994816 1993 4294967295 134512640 135094434 3221224432 3221221456 134677333 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 1993 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 399.91 Current children cumulated vsize (Kb) 10908 [startup+410.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7498 0 0 0 40964 26 0 0 25 0 1 0 1796713070 8994816 2032 4294967295 134512640 135094434 3221224432 3221220208 134600241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2032 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 409.91 Current children cumulated vsize (Kb) 10908 [startup+420.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7498 0 0 0 41964 26 0 0 25 0 1 0 1796713070 8994816 2032 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2032 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 419.91 Current children cumulated vsize (Kb) 10908 [startup+430.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7498 0 0 0 42965 26 0 0 25 0 1 0 1796713070 8994816 2032 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2032 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 429.92 Current children cumulated vsize (Kb) 10908 [startup+440.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7498 0 0 0 43965 26 0 0 25 0 1 0 1796713070 8994816 2032 4294967295 134512640 135094434 3221224432 3221221156 134676608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2032 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 439.92 Current children cumulated vsize (Kb) 10908 [startup+450.042 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7498 0 0 0 44964 28 0 0 25 0 1 0 1796713070 8994816 2032 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2032 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 449.93 Current children cumulated vsize (Kb) 10908 [startup+460.043 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7539 0 0 0 45963 28 0 0 25 0 1 0 1796713070 8994816 2073 4294967295 134512640 135094434 3221224432 3221220144 134676321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2073 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 459.92 Current children cumulated vsize (Kb) 10908 [startup+470.043 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7539 0 0 0 46963 29 0 0 25 0 1 0 1796713070 8994816 2073 4294967295 134512640 135094434 3221224432 3221221688 134677229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2073 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 469.93 Current children cumulated vsize (Kb) 10908 [startup+480.044 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 7712 0 0 0 47963 29 0 0 25 0 1 0 1796713070 8994816 2081 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 2196 2081 145 145 0 2051 0 [pid=10231] vsize: 8784 Current children cumulated CPU time (s) 479.93 Current children cumulated vsize (Kb) 10908 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 16835 0 0 0 48884 68 0 0 25 0 1 0 1796713070 48668672 11188 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 11882 11188 145 145 0 11737 0 [pid=10231] vsize: 47528 Current children cumulated CPU time (s) 489.53 Current children cumulated vsize (Kb) 49652 [startup+500.045 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 16866 0 0 0 49883 69 0 0 25 0 1 0 1796713070 48693248 11219 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10231/statm): 11888 11219 145 145 0 11743 0 [pid=10231] vsize: 47552 Current children cumulated CPU time (s) 499.53 Current children cumulated vsize (Kb) 49676 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 16887 0 0 0 50881 70 0 0 25 0 1 0 1796713070 48717824 11240 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10231/statm): 11894 11240 145 145 0 11749 0 [pid=10231] vsize: 47576 Current children cumulated CPU time (s) 509.52 Current children cumulated vsize (Kb) 49700 [startup+520.047 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 16920 0 0 0 51881 71 0 0 25 0 1 0 1796713070 48881664 11273 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 11934 11273 145 145 0 11789 0 [pid=10231] vsize: 47736 Current children cumulated CPU time (s) 519.53 Current children cumulated vsize (Kb) 49860 [startup+530.048 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 17193 0 0 0 52875 72 0 0 25 0 1 0 1796713070 49967104 11546 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 12199 11546 145 145 0 12054 0 [pid=10231] vsize: 48796 Current children cumulated CPU time (s) 529.48 Current children cumulated vsize (Kb) 50920 [startup+540.049 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 17284 0 0 0 53874 73 0 0 25 0 1 0 1796713070 50327552 11637 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 12287 11637 145 145 0 12142 0 [pid=10231] vsize: 49148 Current children cumulated CPU time (s) 539.48 Current children cumulated vsize (Kb) 51272 [startup+550.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 17338 0 0 0 54874 73 0 0 25 0 1 0 1796713070 50651136 11691 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 12366 11691 145 145 0 12221 0 [pid=10231] vsize: 49464 Current children cumulated CPU time (s) 549.48 Current children cumulated vsize (Kb) 51588 [startup+560.051 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 17655 0 0 0 55869 76 0 0 25 0 1 0 1796713070 51916800 12008 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 12675 12008 145 145 0 12530 0 [pid=10231] vsize: 50700 Current children cumulated CPU time (s) 559.46 Current children cumulated vsize (Kb) 52824 [startup+570.052 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 17917 0 0 0 56864 77 0 0 25 0 1 0 1796713070 52977664 12270 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 12934 12270 145 145 0 12789 0 [pid=10231] vsize: 51736 Current children cumulated CPU time (s) 569.42 Current children cumulated vsize (Kb) 53860 [startup+580.053 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 18192 0 0 0 57859 79 0 0 25 0 1 0 1796713070 54083584 12545 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 13204 12545 145 145 0 13059 0 [pid=10231] vsize: 52816 Current children cumulated CPU time (s) 579.39 Current children cumulated vsize (Kb) 54940 [startup+590.054 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 18509 0 0 0 58853 82 0 0 25 0 1 0 1796713070 55361536 12862 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 13516 12862 145 145 0 13371 0 [pid=10231] vsize: 54064 Current children cumulated CPU time (s) 589.36 Current children cumulated vsize (Kb) 56188 [startup+600.055 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 18893 0 0 0 59845 86 0 0 25 0 1 0 1796713070 57176064 13246 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 13959 13246 145 145 0 13814 0 [pid=10231] vsize: 55836 Current children cumulated CPU time (s) 599.32 Current children cumulated vsize (Kb) 57960 [startup+610.055 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 19214 0 0 0 60839 88 0 0 25 0 1 0 1796713070 58474496 13567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 14276 13567 145 145 0 14131 0 [pid=10231] vsize: 57104 Current children cumulated CPU time (s) 609.28 Current children cumulated vsize (Kb) 59228 [startup+620.055 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 19495 0 0 0 61833 91 0 0 25 0 1 0 1796713070 59609088 13848 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 14553 13848 145 145 0 14408 0 [pid=10231] vsize: 58212 Current children cumulated CPU time (s) 619.25 Current children cumulated vsize (Kb) 60336 [startup+630.057 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 19820 0 0 0 62827 93 0 0 25 0 1 0 1796713070 60928000 14173 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10231/statm): 14875 14173 145 145 0 14730 0 [pid=10231] vsize: 59500 Current children cumulated CPU time (s) 629.21 Current children cumulated vsize (Kb) 61624 [startup+640.058 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 20148 0 0 0 63820 97 0 0 25 0 1 0 1796713070 62255104 14501 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 15199 14501 145 145 0 15054 0 [pid=10231] vsize: 60796 Current children cumulated CPU time (s) 639.18 Current children cumulated vsize (Kb) 62920 [startup+650.059 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 20344 0 0 0 64817 99 0 0 25 0 1 0 1796713070 63049728 14697 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 15393 14697 145 145 0 15248 0 [pid=10231] vsize: 61572 Current children cumulated CPU time (s) 649.17 Current children cumulated vsize (Kb) 63696 [startup+660.06 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 20539 0 0 0 65814 100 0 0 25 0 1 0 1796713070 63852544 14892 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 15589 14892 145 145 0 15444 0 [pid=10231] vsize: 62356 Current children cumulated CPU time (s) 659.15 Current children cumulated vsize (Kb) 64480 [startup+670.06 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 20715 0 0 0 66811 102 0 0 25 0 1 0 1796713070 64565248 15068 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 15763 15068 145 145 0 15618 0 [pid=10231] vsize: 63052 Current children cumulated CPU time (s) 669.14 Current children cumulated vsize (Kb) 65176 [startup+680.061 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 20913 0 0 0 67807 103 0 0 25 0 1 0 1796713070 65359872 15266 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 15957 15266 145 145 0 15812 0 [pid=10231] vsize: 63828 Current children cumulated CPU time (s) 679.11 Current children cumulated vsize (Kb) 65952 [startup+690.062 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 21192 0 0 0 68802 105 0 0 25 0 1 0 1796713070 66486272 15545 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 16232 15545 145 145 0 16087 0 [pid=10231] vsize: 64928 Current children cumulated CPU time (s) 689.08 Current children cumulated vsize (Kb) 67052 [startup+700.064 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 21342 0 0 0 69800 106 0 0 25 0 1 0 1796713070 67092480 15695 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 16380 15695 145 145 0 16235 0 [pid=10231] vsize: 65520 Current children cumulated CPU time (s) 699.07 Current children cumulated vsize (Kb) 67644 [startup+710.065 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 21580 0 0 0 70797 108 0 0 25 0 1 0 1796713070 68050944 15933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 16614 15933 145 145 0 16469 0 [pid=10231] vsize: 66456 Current children cumulated CPU time (s) 709.06 Current children cumulated vsize (Kb) 68580 [startup+720.066 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 21841 0 0 0 71792 110 0 0 25 0 1 0 1796713070 69111808 16194 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 16873 16194 145 145 0 16728 0 [pid=10231] vsize: 67492 Current children cumulated CPU time (s) 719.03 Current children cumulated vsize (Kb) 69616 [startup+730.067 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 22080 0 0 0 72786 112 0 0 25 0 1 0 1796713070 70078464 16433 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 17109 16433 145 145 0 16964 0 [pid=10231] vsize: 68436 Current children cumulated CPU time (s) 728.99 Current children cumulated vsize (Kb) 70560 [startup+740.068 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 22314 0 0 0 73783 114 0 0 25 0 1 0 1796713070 71020544 16667 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 17339 16667 145 145 0 17194 0 [pid=10231] vsize: 69356 Current children cumulated CPU time (s) 738.98 Current children cumulated vsize (Kb) 71480 [startup+750.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 22523 0 0 0 74779 115 0 0 25 0 1 0 1796713070 71860224 16876 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10231/statm): 17544 16876 145 145 0 17399 0 [pid=10231] vsize: 70176 Current children cumulated CPU time (s) 748.95 Current children cumulated vsize (Kb) 72300 [startup+760.071 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 22776 0 0 0 75773 117 0 0 25 0 1 0 1796713070 72876032 17129 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10231/statm): 17792 17129 145 145 0 17647 0 [pid=10231] vsize: 71168 Current children cumulated CPU time (s) 758.91 Current children cumulated vsize (Kb) 73292 [startup+770.072 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 23047 0 0 0 76768 119 0 0 25 0 1 0 1796713070 73969664 17400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 18059 17400 145 145 0 17914 0 [pid=10231] vsize: 72236 Current children cumulated CPU time (s) 768.88 Current children cumulated vsize (Kb) 74360 [startup+780.073 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 23230 0 0 0 77765 121 0 0 25 0 1 0 1796713070 75231232 17583 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 18367 17583 145 145 0 18222 0 [pid=10231] vsize: 73468 Current children cumulated CPU time (s) 778.87 Current children cumulated vsize (Kb) 75592 [startup+790.073 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 23440 0 0 0 78762 122 0 0 25 0 1 0 1796713070 76079104 17793 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 18574 17793 145 145 0 18429 0 [pid=10231] vsize: 74296 Current children cumulated CPU time (s) 788.85 Current children cumulated vsize (Kb) 76420 [startup+800.075 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 23672 0 0 0 79757 125 0 0 25 0 1 0 1796713070 77017088 18025 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 18803 18025 145 145 0 18658 0 [pid=10231] vsize: 75212 Current children cumulated CPU time (s) 798.83 Current children cumulated vsize (Kb) 77336 [startup+810.076 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 23892 0 0 0 80753 127 0 0 25 0 1 0 1796713070 77914112 18245 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 19022 18245 145 145 0 18877 0 [pid=10231] vsize: 76088 Current children cumulated CPU time (s) 808.81 Current children cumulated vsize (Kb) 78212 [startup+820.077 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 24111 0 0 0 81750 128 0 0 25 0 1 0 1796713070 78794752 18464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 19237 18464 145 145 0 19092 0 [pid=10231] vsize: 76948 Current children cumulated CPU time (s) 818.79 Current children cumulated vsize (Kb) 79072 [startup+830.078 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 24366 0 0 0 82744 130 0 0 25 0 1 0 1796713070 79822848 18719 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 19488 18719 145 145 0 19343 0 [pid=10231] vsize: 77952 Current children cumulated CPU time (s) 828.75 Current children cumulated vsize (Kb) 80076 [startup+840.079 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 24569 0 0 0 83741 131 0 0 25 0 1 0 1796713070 80642048 18922 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 19688 18922 145 145 0 19543 0 [pid=10231] vsize: 78752 Current children cumulated CPU time (s) 838.73 Current children cumulated vsize (Kb) 80876 [startup+850.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 24760 0 0 0 84738 133 0 0 25 0 1 0 1796713070 81416192 19113 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 19877 19113 145 145 0 19732 0 [pid=10231] vsize: 79508 Current children cumulated CPU time (s) 848.72 Current children cumulated vsize (Kb) 81632 [startup+860.081 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 24955 0 0 0 85734 134 0 0 25 0 1 0 1796713070 82206720 19308 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 20070 19308 145 145 0 19925 0 [pid=10231] vsize: 80280 Current children cumulated CPU time (s) 858.69 Current children cumulated vsize (Kb) 82404 [startup+870.082 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 25135 0 0 0 86731 136 0 0 25 0 1 0 1796713070 82931712 19488 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 20247 19488 145 145 0 20102 0 [pid=10231] vsize: 80988 Current children cumulated CPU time (s) 868.68 Current children cumulated vsize (Kb) 83112 [startup+880.083 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 25350 0 0 0 87728 137 0 0 25 0 1 0 1796713070 83808256 19703 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 20461 19703 145 145 0 20316 0 [pid=10231] vsize: 81844 Current children cumulated CPU time (s) 878.66 Current children cumulated vsize (Kb) 83968 [startup+890.084 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 25562 0 0 0 88724 138 0 0 25 0 1 0 1796713070 84672512 19915 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 20672 19915 145 145 0 20527 0 [pid=10231] vsize: 82688 Current children cumulated CPU time (s) 888.63 Current children cumulated vsize (Kb) 84812 [startup+900.086 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 25734 0 0 0 89722 139 0 0 23 0 1 0 1796713070 85368832 20087 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 20842 20087 145 145 0 20697 0 [pid=10231] vsize: 83368 Current children cumulated CPU time (s) 898.62 Current children cumulated vsize (Kb) 85492 [startup+910.087 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 25866 0 0 0 90719 140 0 0 25 0 1 0 1796713070 85921792 20219 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 20977 20219 145 145 0 20832 0 [pid=10231] vsize: 83908 Current children cumulated CPU time (s) 908.6 Current children cumulated vsize (Kb) 86032 [startup+920.088 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 26000 0 0 0 91717 141 0 0 25 0 1 0 1796713070 86462464 20353 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 21109 20353 145 145 0 20964 0 [pid=10231] vsize: 84436 Current children cumulated CPU time (s) 918.59 Current children cumulated vsize (Kb) 86560 [startup+930.089 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 26154 0 0 0 92714 142 0 0 25 0 1 0 1796713070 87085056 20507 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 21261 20507 145 145 0 21116 0 [pid=10231] vsize: 85044 Current children cumulated CPU time (s) 928.57 Current children cumulated vsize (Kb) 87168 [startup+940.09 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 26301 0 0 0 93711 143 0 0 25 0 1 0 1796713070 87683072 20654 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 21407 20654 145 145 0 21262 0 [pid=10231] vsize: 85628 Current children cumulated CPU time (s) 938.55 Current children cumulated vsize (Kb) 87752 [startup+950.092 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 26445 0 0 0 94708 145 0 0 25 0 1 0 1796713070 88272896 20798 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 21551 20798 145 145 0 21406 0 [pid=10231] vsize: 86204 Current children cumulated CPU time (s) 948.54 Current children cumulated vsize (Kb) 88328 [startup+960.093 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 26589 0 0 0 95706 146 0 0 25 0 1 0 1796713070 88854528 20942 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 21693 20942 145 145 0 21548 0 [pid=10231] vsize: 86772 Current children cumulated CPU time (s) 958.53 Current children cumulated vsize (Kb) 88896 [startup+970.093 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 26734 0 0 0 96704 147 0 0 25 0 1 0 1796713070 89436160 21087 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 21835 21087 145 145 0 21690 0 [pid=10231] vsize: 87340 Current children cumulated CPU time (s) 968.52 Current children cumulated vsize (Kb) 89464 [startup+980.095 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 26868 0 0 0 97701 148 0 0 25 0 1 0 1796713070 89972736 21221 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 21966 21221 145 145 0 21821 0 [pid=10231] vsize: 87864 Current children cumulated CPU time (s) 978.5 Current children cumulated vsize (Kb) 89988 [startup+990.096 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 27023 0 0 0 98699 149 0 0 25 0 1 0 1796713070 90599424 21376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 22119 21376 145 145 0 21974 0 [pid=10231] vsize: 88476 Current children cumulated CPU time (s) 988.49 Current children cumulated vsize (Kb) 90600 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 27198 0 0 0 99696 151 0 0 25 0 1 0 1796713070 91312128 21551 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 22293 21551 145 145 0 22148 0 [pid=10231] vsize: 89172 Current children cumulated CPU time (s) 998.48 Current children cumulated vsize (Kb) 91296 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 27340 0 0 0 100693 152 0 0 25 0 1 0 1796713070 91910144 21693 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10231/statm): 22439 21693 145 145 0 22294 0 [pid=10231] vsize: 89756 Current children cumulated CPU time (s) 1008.46 Current children cumulated vsize (Kb) 91880 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 27464 0 0 0 101690 153 0 0 25 0 1 0 1796713070 92405760 21817 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 22560 21817 145 145 0 22415 0 [pid=10231] vsize: 90240 Current children cumulated CPU time (s) 1018.44 Current children cumulated vsize (Kb) 92364 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 27581 0 0 0 102688 153 0 0 25 0 1 0 1796713070 92876800 21934 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 22675 21934 145 145 0 22530 0 [pid=10231] vsize: 90700 Current children cumulated CPU time (s) 1028.42 Current children cumulated vsize (Kb) 92824 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 27698 0 0 0 103686 154 0 0 25 0 1 0 1796713070 93356032 22051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 22792 22051 145 145 0 22647 0 [pid=10231] vsize: 91168 Current children cumulated CPU time (s) 1038.41 Current children cumulated vsize (Kb) 93292 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 27823 0 0 0 104683 156 0 0 25 0 1 0 1796713070 93863936 22176 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 22916 22176 145 145 0 22771 0 [pid=10231] vsize: 91664 Current children cumulated CPU time (s) 1048.4 Current children cumulated vsize (Kb) 93788 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.97 1/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) T 10227 10227 8263 0 -1 0 27939 0 0 0 105681 158 0 0 25 0 1 0 1796713070 94347264 22292 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23034 22292 145 145 0 22889 0 [pid=10231] vsize: 92136 Current children cumulated CPU time (s) 1058.4 Current children cumulated vsize (Kb) 94260 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 28057 0 0 0 106678 159 0 0 25 0 1 0 1796713070 94818304 22410 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23149 22410 145 145 0 23004 0 [pid=10231] vsize: 92596 Current children cumulated CPU time (s) 1068.38 Current children cumulated vsize (Kb) 94720 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 28203 0 0 0 107676 160 0 0 25 0 1 0 1796713070 95412224 22556 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23294 22556 145 145 0 23149 0 [pid=10231] vsize: 93176 Current children cumulated CPU time (s) 1078.37 Current children cumulated vsize (Kb) 95300 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 28358 0 0 0 108674 161 0 0 25 0 1 0 1796713070 96043008 22711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23448 22711 145 145 0 23303 0 [pid=10231] vsize: 93792 Current children cumulated CPU time (s) 1088.36 Current children cumulated vsize (Kb) 95916 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 28513 0 0 0 109671 162 0 0 25 0 1 0 1796713070 96681984 22866 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23604 22866 145 145 0 23459 0 [pid=10231] vsize: 94416 Current children cumulated CPU time (s) 1098.34 Current children cumulated vsize (Kb) 96540 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 28640 0 0 0 110667 163 0 0 25 0 1 0 1796713070 97189888 22993 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23728 22993 145 145 0 23583 0 [pid=10231] vsize: 94912 Current children cumulated CPU time (s) 1108.31 Current children cumulated vsize (Kb) 97036 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 28763 0 0 0 111665 165 0 0 25 0 1 0 1796713070 97689600 23116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23850 23116 145 145 0 23705 0 [pid=10231] vsize: 95400 Current children cumulated CPU time (s) 1118.31 Current children cumulated vsize (Kb) 97524 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 28885 0 0 0 112662 166 0 0 25 0 1 0 1796713070 98197504 23238 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 23974 23238 145 145 0 23829 0 [pid=10231] vsize: 95896 Current children cumulated CPU time (s) 1128.29 Current children cumulated vsize (Kb) 98020 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29007 0 0 0 113661 167 0 0 25 0 1 0 1796713070 98693120 23360 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24095 23360 145 145 0 23950 0 [pid=10231] vsize: 96380 Current children cumulated CPU time (s) 1138.29 Current children cumulated vsize (Kb) 98504 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29143 0 0 0 114659 168 0 0 25 0 1 0 1796713070 99254272 23496 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24232 23496 145 145 0 24087 0 [pid=10231] vsize: 96928 Current children cumulated CPU time (s) 1148.28 Current children cumulated vsize (Kb) 99052 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29306 0 0 0 115656 170 0 0 25 0 1 0 1796713070 99909632 23659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24392 23659 145 145 0 24247 0 [pid=10231] vsize: 97568 Current children cumulated CPU time (s) 1158.27 Current children cumulated vsize (Kb) 99692 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29413 0 0 0 116655 170 0 0 25 0 1 0 1796713070 100347904 23766 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24499 23766 145 145 0 24354 0 [pid=10231] vsize: 97996 Current children cumulated CPU time (s) 1168.26 Current children cumulated vsize (Kb) 100120 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29506 0 0 0 117654 171 0 0 25 0 1 0 1796713070 100720640 23859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24590 23859 145 145 0 24445 0 [pid=10231] vsize: 98360 Current children cumulated CPU time (s) 1178.26 Current children cumulated vsize (Kb) 100484 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29605 0 0 0 118651 172 0 0 25 0 1 0 1796713070 101126144 23958 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24689 23958 145 145 0 24544 0 [pid=10231] vsize: 98756 Current children cumulated CPU time (s) 1188.24 Current children cumulated vsize (Kb) 100880 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29716 0 0 0 119650 173 0 0 25 0 1 0 1796713070 101576704 24069 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24799 24069 145 145 0 24654 0 [pid=10231] vsize: 99196 Current children cumulated CPU time (s) 1198.24 Current children cumulated vsize (Kb) 101320 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29815 0 0 0 120648 173 0 0 25 0 1 0 1796713070 101974016 24168 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24896 24168 145 145 0 24751 0 [pid=10231] vsize: 99584 Current children cumulated CPU time (s) 1208.22 Current children cumulated vsize (Kb) 101708 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 10231 Raw data (/proc/10227/stat): 10227 (minisat+_script) S 10226 10227 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796713066 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10227/statm): 531 226 485 147 0 384 0 [pid=10227] vsize: 2124 Raw data (/proc/10231/stat): 10231 (minisat+_64-bit) R 10227 10227 8263 0 -1 0 29815 0 0 0 120648 173 0 0 25 0 1 0 1796713070 101974016 24168 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10231/statm): 24896 24168 145 145 0 24751 0 [pid=10231] vsize: 99584 Current children cumulated CPU time (s) 1208.22 Current children cumulated vsize (Kb) 101708 Sending SIGTERM to -10227 Sleeping 2 seconds One traced child (pid=10227) ended because it received signal 15 (SIGTERM) One traced child (pid=10231) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1208.28 CPU user time (s): 1206.49 CPU system time (s): 1.78573 CPU usage (%): 99.8434 Max. virtual memory (cumulated for all children) (Kb): 101708
ERROR: no interpretation found !