Name | submitted/aloul/FPGA_SAT05/normalized-chnl20_30_pb.cnf.cr.opb |
MD5SUM | afcc4289aafaea265ed2d465965a3342 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 31 |
Number of bits of the biggest sum of numbers | 5 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.040993 |
Number of variables | 1200 |
Total number of constraints | 100 |
Number of constraints which are clauses | 60 |
Number of constraints which are cardinality constraints (but not clauses) | 40 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 30 |
LAUNCH ON wulflinc31 THE 2005-09-18 12:24:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2352 boxname=wulflinc31 idbench=8 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: afcc4289aafaea265ed2d465965a3342 /oldhome/oroussel/tmp/wulflinc31/normalized-chnl20_30_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-chnl20_30_pb.cnf.cr.opb IDLAUNCH: 2352 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 717104 kB Buffers: 35348 kB Cached: 251616 kB SwapCached: 1016 kB Active: 92492 kB Inactive: 197192 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 716852 kB SwapTotal: 2097892 kB SwapFree: 2096404 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5768 kB Slab: 22164 kB Committed_AS: 64340 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 12:44:15 (client local time) WITH STATUS 0 IN 1209.58 SECONDS stats: 2352 7 1209.58 0
c Parsing PB file... c Converting 100 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ............................................................ c ---[ 39]---> BDD-cost: 57 c ---[ 38]---> BDD-cost: 57 c ---[ 37]---> BDD-cost: 57 c ---[ 36]---> BDD-cost: 57 c ---[ 35]---> BDD-cost: 57 c ---[ 34]---> BDD-cost: 57 c ---[ 33]---> BDD-cost: 57 c ---[ 32]---> BDD-cost: 57 c ---[ 31]---> BDD-cost: 57 c ---[ 30]---> BDD-cost: 57 c ---[ 29]---> BDD-cost: 57 c ---[ 28]---> BDD-cost: 57 c ---[ 27]---> BDD-cost: 57 c ---[ 26]---> BDD-cost: 57 c ---[ 25]---> BDD-cost: 57 c ---[ 24]---> BDD-cost: 57 c ---[ 23]---> BDD-cost: 57 c ---[ 22]---> BDD-cost: 57 c ---[ 21]---> BDD-cost: 57 c ---[ 20]---> BDD-cost: 57 c ---[ 19]---> BDD-cost: 57 c ---[ 18]---> BDD-cost: 57 c ---[ 17]---> BDD-cost: 57 c ---[ 16]---> BDD-cost: 57 c ---[ 15]---> BDD-cost: 57 c ---[ 14]---> BDD-cost: 57 c ---[ 13]---> BDD-cost: 57 c ---[ 12]---> BDD-cost: 57 c ---[ 11]---> BDD-cost: 57 c ---[ 10]---> BDD-cost: 57 c ---[ 9]---> BDD-cost: 57 c ---[ 8]---> BDD-cost: 57 c ---[ 7]---> BDD-cost: 57 c ---[ 6]---> BDD-cost: 57 c ---[ 5]---> BDD-cost: 57 c ---[ 4]---> BDD-cost: 57 c ---[ 3]---> BDD-cost: 57 c ---[ 2]---> BDD-cost: 57 c ---[ 1]---> BDD-cost: 57 c ---[ 0]---> BDD-cost: 57 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 5700 15880 | 1900 0 0 nan | 0.000 % | c | 100 | 5700 15880 | 2090 100 8350 83.5 | 1.149 % | c | 254 | 5700 15880 | 2299 254 20183 79.5 | 1.149 % | c | 483 | 5700 15880 | 2528 483 43595 90.3 | 1.150 % | c | 820 | 5700 15880 | 2781 820 74636 91.0 | 1.149 % | c | 1326 | 5700 15880 | 3059 1326 152844 115.3 | 1.149 % | c | 2085 | 5700 15880 | 3365 2085 236742 113.5 | 1.149 % | c | 3224 | 5700 15880 | 3702 3224 390616 121.2 | 1.149 % | c | 4934 | 5700 15880 | 4072 2499 282510 113.0 | 1.149 % | c | 7497 | 5700 15880 | 4480 5062 635699 125.6 | 1.149 % | c | 11341 | 5700 15880 | 4928 3602 393130 109.1 | 1.149 % | c | 17107 | 5700 15880 | 5420 3198 429474 134.3 | 1.149 % | c | 25758 | 5700 15880 | 5963 5184 809083 156.1 | 1.149 % | c | 38734 | 5700 15880 | 6559 4258 595019 139.7 | 1.149 % | c | 58195 | 5700 15880 | 7215 4350 474363 109.0 | 1.149 % | c | 87389 | 5700 15880 | 7936 5401 906885 167.9 | 1.149 % | c | 131180 | 5700 15880 | 8730 8927 1807067 202.4 | 1.150 % | c | 196867 | 5700 15880 | 9603 7833 1793666 229.0 | 1.149 % | c | 295396 | 5700 15880 | 10563 5671 840337 148.2 | 1.149 % | c | 443189 | 5700 15880 | 11620 8324 1522755 182.9 | 1.149 % | c | 664881 | 5700 15880 | 12782 7923 1541577 194.6 | 1.149 % |
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/11836/stat): 11836 (minisat+_script) R 11835 11836 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841190087 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/11836/statm): 174 3 169 147 0 27 0 [pid=11836] 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=11837 New process pid=11838 New process pid=11839 execve syscall for /bin/sed executable One traced child (pid=11838) 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=11839) exited with status: 0 One traced child (pid=11837) exited with status: 0 New process pid=11840 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-chnl20_30_pb.cnf.cr.opb [startup+10.006 s] Raw data (loadavg): 0.93 0.98 0.96 2/58 11840 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1258 0 3 0 966 7 0 0 25 0 1 0 1841190092 5480448 1248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 1338 1248 145 145 0 1193 0 [pid=11840] vsize: 5352 Current children cumulated CPU time (s) 9.75 Current children cumulated vsize (Kb) 7476 [startup+20.0069 s] Raw data (loadavg): 0.94 0.98 0.96 2/58 11840 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1617 0 3 0 1962 9 0 0 25 0 1 0 1841190092 6971392 1607 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 1702 1607 145 145 0 1557 0 [pid=11840] vsize: 6808 Current children cumulated CPU time (s) 19.73 Current children cumulated vsize (Kb) 8932 [startup+30.0078 s] Raw data (loadavg): 0.95 0.98 0.96 2/58 11842 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1747 0 3 0 2959 10 0 0 25 0 1 0 1841190092 7516160 1737 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 1835 1737 145 145 0 1690 0 [pid=11840] vsize: 7340 Current children cumulated CPU time (s) 29.71 Current children cumulated vsize (Kb) 9464 [startup+40.0087 s] Raw data (loadavg): 0.96 0.98 0.96 2/58 11842 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1881 0 3 0 3958 11 0 0 25 0 1 0 1841190092 8085504 1871 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 1974 1871 145 145 0 1829 0 [pid=11840] vsize: 7896 Current children cumulated CPU time (s) 39.71 Current children cumulated vsize (Kb) 10020 [startup+50.0097 s] Raw data (loadavg): 0.96 0.98 0.96 2/58 11842 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1913 0 3 0 4958 11 0 0 25 0 1 0 1841190092 8241152 1903 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2012 1903 145 145 0 1867 0 [pid=11840] vsize: 8048 Current children cumulated CPU time (s) 49.71 Current children cumulated vsize (Kb) 10172 [startup+60.0106 s] Raw data (loadavg): 0.97 0.98 0.96 2/58 11842 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 1939 0 3 0 5958 12 0 0 25 0 1 0 1841190092 8372224 1929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2044 1929 145 145 0 1899 0 [pid=11840] vsize: 8176 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 10300 [startup+70.0115 s] Raw data (loadavg): 0.97 0.98 0.96 2/58 11842 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2138 0 3 0 6956 12 0 0 25 0 1 0 1841190092 9224192 2128 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2252 2128 145 145 0 2107 0 [pid=11840] vsize: 9008 Current children cumulated CPU time (s) 69.7 Current children cumulated vsize (Kb) 11132 [startup+80.0125 s] Raw data (loadavg): 0.98 0.98 0.96 2/58 11842 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2325 0 3 0 7953 13 0 0 25 0 1 0 1841190092 9998336 2315 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2441 2315 145 145 0 2296 0 [pid=11840] vsize: 9764 Current children cumulated CPU time (s) 79.68 Current children cumulated vsize (Kb) 11888 [startup+90.0134 s] Raw data (loadavg): 0.98 0.98 0.96 2/58 11844 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2361 0 3 0 8953 14 0 0 25 0 1 0 1841190092 10162176 2351 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2481 2351 145 145 0 2336 0 [pid=11840] vsize: 9924 Current children cumulated CPU time (s) 89.69 Current children cumulated vsize (Kb) 12048 [startup+100.014 s] Raw data (loadavg): 0.98 0.98 0.96 2/58 11844 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2741 0 3 0 9948 16 0 0 25 0 1 0 1841190092 11722752 2731 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2862 2731 145 145 0 2717 0 [pid=11840] vsize: 11448 Current children cumulated CPU time (s) 99.66 Current children cumulated vsize (Kb) 13572 [startup+110.016 s] Raw data (loadavg): 0.98 0.98 0.96 2/58 11844 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2781 0 3 0 10948 16 0 0 25 0 1 0 1841190092 11902976 2771 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2906 2771 145 145 0 2761 0 [pid=11840] vsize: 11624 Current children cumulated CPU time (s) 109.66 Current children cumulated vsize (Kb) 13748 [startup+120.017 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11844 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2863 0 3 0 11947 17 0 0 25 0 1 0 1841190092 12251136 2853 4294967295 134512640 135094434 3221224432 3221223104 134555291 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2991 2853 145 145 0 2846 0 [pid=11840] vsize: 11964 Current children cumulated CPU time (s) 119.66 Current children cumulated vsize (Kb) 14088 [startup+130.017 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11844 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2863 0 3 0 12947 17 0 0 25 0 1 0 1841190092 12251136 2853 4294967295 134512640 135094434 3221224432 3221223104 134556426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 2991 2853 145 145 0 2846 0 [pid=11840] vsize: 11964 Current children cumulated CPU time (s) 129.66 Current children cumulated vsize (Kb) 14088 [startup+140.018 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11844 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 2918 0 3 0 13947 18 0 0 25 0 1 0 1841190092 12480512 2908 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 3047 2908 145 145 0 2902 0 [pid=11840] vsize: 12188 Current children cumulated CPU time (s) 139.67 Current children cumulated vsize (Kb) 14312 [startup+150.019 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11846 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3251 0 3 0 14943 19 0 0 25 0 1 0 1841190092 13856768 3241 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 3383 3241 145 145 0 3238 0 [pid=11840] vsize: 13532 Current children cumulated CPU time (s) 149.64 Current children cumulated vsize (Kb) 15656 [startup+160.02 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11846 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3486 0 3 0 15940 21 0 0 25 0 1 0 1841190092 14839808 3476 4294967295 134512640 135094434 3221224432 3221223024 134785070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 3623 3476 145 145 0 3478 0 [pid=11840] vsize: 14492 Current children cumulated CPU time (s) 159.63 Current children cumulated vsize (Kb) 16616 [startup+170.021 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11846 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3707 0 3 0 16934 23 0 0 25 0 1 0 1841190092 15749120 3697 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 3845 3697 145 145 0 3700 0 [pid=11840] vsize: 15380 Current children cumulated CPU time (s) 169.59 Current children cumulated vsize (Kb) 17504 [startup+180.022 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11846 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3840 0 3 0 17932 24 0 0 25 0 1 0 1841190092 16322560 3830 4294967295 134512640 135094434 3221224432 3221223024 134557336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 3985 3830 145 145 0 3840 0 [pid=11840] vsize: 15940 Current children cumulated CPU time (s) 179.58 Current children cumulated vsize (Kb) 18064 [startup+190.024 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11846 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3867 0 3 0 18931 25 0 0 25 0 1 0 1841190092 16433152 3857 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4012 3857 145 145 0 3867 0 [pid=11840] vsize: 16048 Current children cumulated CPU time (s) 189.58 Current children cumulated vsize (Kb) 18172 [startup+200.025 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11846 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3868 0 3 0 19931 25 0 0 25 0 1 0 1841190092 16433152 3858 4294967295 134512640 135094434 3221224432 3221223024 134551885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4012 3858 145 145 0 3867 0 [pid=11840] vsize: 16048 Current children cumulated CPU time (s) 199.58 Current children cumulated vsize (Kb) 18172 [startup+210.026 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11848 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3886 0 3 0 20930 26 0 0 25 0 1 0 1841190092 16531456 3876 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4036 3876 145 145 0 3891 0 [pid=11840] vsize: 16144 Current children cumulated CPU time (s) 209.58 Current children cumulated vsize (Kb) 18268 [startup+220.027 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11848 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3892 0 3 0 21930 26 0 0 25 0 1 0 1841190092 16564224 3882 4294967295 134512640 135094434 3221224432 3221222976 134779266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4044 3882 145 145 0 3899 0 [pid=11840] vsize: 16176 Current children cumulated CPU time (s) 219.58 Current children cumulated vsize (Kb) 18300 [startup+230.027 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11848 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 3892 0 3 0 22929 27 0 0 25 0 1 0 1841190092 16564224 3882 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4044 3882 145 145 0 3899 0 [pid=11840] vsize: 16176 Current children cumulated CPU time (s) 229.58 Current children cumulated vsize (Kb) 18300 [startup+240.028 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11848 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4045 0 3 0 23927 28 0 0 25 0 1 0 1841190092 17203200 4035 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4200 4035 145 145 0 4055 0 [pid=11840] vsize: 16800 Current children cumulated CPU time (s) 239.57 Current children cumulated vsize (Kb) 18924 [startup+250.029 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11848 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4075 0 3 0 24927 28 0 0 25 0 1 0 1841190092 17342464 4065 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4234 4065 145 145 0 4089 0 [pid=11840] vsize: 16936 Current children cumulated CPU time (s) 249.57 Current children cumulated vsize (Kb) 19060 [startup+260.031 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11848 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4222 0 3 0 25925 29 0 0 25 0 1 0 1841190092 17960960 4212 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4212 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 259.56 Current children cumulated vsize (Kb) 19664 [startup+270.032 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11850 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4223 0 3 0 26924 30 0 0 25 0 1 0 1841190092 17960960 4213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4213 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 269.56 Current children cumulated vsize (Kb) 19664 [startup+280.033 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11850 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4223 0 3 0 27923 30 0 0 25 0 1 0 1841190092 17960960 4213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4213 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 279.55 Current children cumulated vsize (Kb) 19664 [startup+290.035 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11850 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4224 0 3 0 28923 31 0 0 25 0 1 0 1841190092 17960960 4214 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4214 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 289.56 Current children cumulated vsize (Kb) 19664 [startup+300.036 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11850 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4224 0 3 0 29922 32 0 0 25 0 1 0 1841190092 17960960 4214 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4214 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 299.56 Current children cumulated vsize (Kb) 19664 [startup+310.037 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11850 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4226 0 3 0 30922 32 0 0 25 0 1 0 1841190092 17960960 4216 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4216 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 309.56 Current children cumulated vsize (Kb) 19664 [startup+320.038 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11850 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 31922 32 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 319.56 Current children cumulated vsize (Kb) 19664 [startup+330.039 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11852 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 32921 33 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 329.56 Current children cumulated vsize (Kb) 19664 [startup+340.04 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11852 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 33921 33 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 339.56 Current children cumulated vsize (Kb) 19664 [startup+350.041 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11852 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 34920 34 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 349.56 Current children cumulated vsize (Kb) 19664 [startup+360.043 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11852 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 35920 34 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 359.56 Current children cumulated vsize (Kb) 19664 [startup+370.044 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11852 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 36920 35 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 369.57 Current children cumulated vsize (Kb) 19664 [startup+380.044 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11852 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 37919 35 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 379.56 Current children cumulated vsize (Kb) 19664 [startup+390.045 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11854 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 38918 36 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 389.56 Current children cumulated vsize (Kb) 19664 [startup+400.046 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11854 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 39918 36 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 399.56 Current children cumulated vsize (Kb) 19664 [startup+410.048 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11854 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 40917 37 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 409.56 Current children cumulated vsize (Kb) 19664 [startup+420.049 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11854 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 41917 37 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 419.56 Current children cumulated vsize (Kb) 19664 [startup+430.05 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11854 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 42916 38 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 429.56 Current children cumulated vsize (Kb) 19664 [startup+440.052 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11854 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4227 0 3 0 43916 38 0 0 25 0 1 0 1841190092 17960960 4217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4217 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 439.56 Current children cumulated vsize (Kb) 19664 [startup+450.053 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11856 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 44915 39 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 449.56 Current children cumulated vsize (Kb) 19664 [startup+460.055 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11856 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 45915 39 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 459.56 Current children cumulated vsize (Kb) 19664 [startup+470.056 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11856 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 46915 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 469.57 Current children cumulated vsize (Kb) 19664 [startup+480.057 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11856 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 47915 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 479.57 Current children cumulated vsize (Kb) 19664 [startup+490.059 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11856 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 48914 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 489.56 Current children cumulated vsize (Kb) 19664 [startup+500.06 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11856 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4228 0 3 0 49914 40 0 0 25 0 1 0 1841190092 17960960 4218 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4385 4218 145 145 0 4240 0 [pid=11840] vsize: 17540 Current children cumulated CPU time (s) 499.56 Current children cumulated vsize (Kb) 19664 [startup+510.06 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11858 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4229 0 3 0 50915 40 0 0 25 0 1 0 1841190092 17965056 4219 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4386 4219 145 145 0 4241 0 [pid=11840] vsize: 17544 Current children cumulated CPU time (s) 509.57 Current children cumulated vsize (Kb) 19668 [startup+520.061 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11858 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4290 0 3 0 51914 41 0 0 25 0 1 0 1841190092 18214912 4280 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4447 4280 145 145 0 4302 0 [pid=11840] vsize: 17788 Current children cumulated CPU time (s) 519.57 Current children cumulated vsize (Kb) 19912 [startup+530.062 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11858 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 52913 41 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0 [pid=11840] vsize: 17788 Current children cumulated CPU time (s) 529.56 Current children cumulated vsize (Kb) 19912 [startup+540.063 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11858 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 53913 42 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0 [pid=11840] vsize: 17788 Current children cumulated CPU time (s) 539.57 Current children cumulated vsize (Kb) 19912 [startup+550.064 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11858 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 54912 42 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0 [pid=11840] vsize: 17788 Current children cumulated CPU time (s) 549.56 Current children cumulated vsize (Kb) 19912 [startup+560.066 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11858 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4291 0 3 0 55912 42 0 0 25 0 1 0 1841190092 18214912 4281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4447 4281 145 145 0 4302 0 [pid=11840] vsize: 17788 Current children cumulated CPU time (s) 559.56 Current children cumulated vsize (Kb) 19912 [startup+570.067 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11862 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4295 0 3 0 56913 42 0 0 25 0 1 0 1841190092 18239488 4285 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4453 4285 145 145 0 4308 0 [pid=11840] vsize: 17812 Current children cumulated CPU time (s) 569.57 Current children cumulated vsize (Kb) 19936 [startup+580.068 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11862 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4295 0 3 0 57913 42 0 0 25 0 1 0 1841190092 18239488 4285 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4453 4285 145 145 0 4308 0 [pid=11840] vsize: 17812 Current children cumulated CPU time (s) 579.57 Current children cumulated vsize (Kb) 19936 [startup+590.069 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11862 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4306 0 3 0 58913 42 0 0 25 0 1 0 1841190092 18305024 4296 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4469 4296 145 145 0 4324 0 [pid=11840] vsize: 17876 Current children cumulated CPU time (s) 589.57 Current children cumulated vsize (Kb) 20000 [startup+600.07 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11862 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4313 0 3 0 59913 42 0 0 25 0 1 0 1841190092 18337792 4303 4294967295 134512640 135094434 3221224432 3221223024 134551876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4477 4303 145 145 0 4332 0 [pid=11840] vsize: 17908 Current children cumulated CPU time (s) 599.57 Current children cumulated vsize (Kb) 20032 [startup+610.071 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11862 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4313 0 3 0 60914 42 0 0 25 0 1 0 1841190092 18337792 4303 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4477 4303 145 145 0 4332 0 [pid=11840] vsize: 17908 Current children cumulated CPU time (s) 609.58 Current children cumulated vsize (Kb) 20032 [startup+620.072 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11862 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4350 0 3 0 61913 43 0 0 25 0 1 0 1841190092 18509824 4340 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4519 4340 145 145 0 4374 0 [pid=11840] vsize: 18076 Current children cumulated CPU time (s) 619.58 Current children cumulated vsize (Kb) 20200 [startup+630.073 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11866 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4414 0 3 0 62912 44 0 0 25 0 1 0 1841190092 18796544 4404 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4589 4404 145 145 0 4444 0 [pid=11840] vsize: 18356 Current children cumulated CPU time (s) 629.58 Current children cumulated vsize (Kb) 20480 [startup+640.074 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11866 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4425 0 3 0 63912 44 0 0 25 0 1 0 1841190092 18862080 4415 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4605 4415 145 145 0 4460 0 [pid=11840] vsize: 18420 Current children cumulated CPU time (s) 639.58 Current children cumulated vsize (Kb) 20544 [startup+650.074 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11866 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4425 0 3 0 64912 44 0 0 25 0 1 0 1841190092 18862080 4415 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4605 4415 145 145 0 4460 0 [pid=11840] vsize: 18420 Current children cumulated CPU time (s) 649.58 Current children cumulated vsize (Kb) 20544 [startup+660.076 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11866 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4431 0 3 0 65912 44 0 0 25 0 1 0 1841190092 18894848 4421 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4613 4421 145 145 0 4468 0 [pid=11840] vsize: 18452 Current children cumulated CPU time (s) 659.58 Current children cumulated vsize (Kb) 20576 [startup+670.076 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11866 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4437 0 3 0 66913 44 0 0 25 0 1 0 1841190092 18927616 4427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4621 4427 145 145 0 4476 0 [pid=11840] vsize: 18484 Current children cumulated CPU time (s) 669.59 Current children cumulated vsize (Kb) 20608 [startup+680.077 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11866 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4531 0 3 0 67911 44 0 0 25 0 1 0 1841190092 19324928 4521 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4718 4521 145 145 0 4573 0 [pid=11840] vsize: 18872 Current children cumulated CPU time (s) 679.57 Current children cumulated vsize (Kb) 20996 [startup+690.078 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11868 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4544 0 3 0 68911 44 0 0 25 0 1 0 1841190092 19390464 4534 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4734 4534 145 145 0 4589 0 [pid=11840] vsize: 18936 Current children cumulated CPU time (s) 689.57 Current children cumulated vsize (Kb) 21060 [startup+700.079 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11868 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4544 0 3 0 69911 45 0 0 25 0 1 0 1841190092 19390464 4534 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4734 4534 145 145 0 4589 0 [pid=11840] vsize: 18936 Current children cumulated CPU time (s) 699.58 Current children cumulated vsize (Kb) 21060 [startup+710.08 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11868 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4651 0 3 0 70910 45 0 0 25 0 1 0 1841190092 19832832 4641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4842 4641 145 145 0 4697 0 [pid=11840] vsize: 19368 Current children cumulated CPU time (s) 709.57 Current children cumulated vsize (Kb) 21492 [startup+720.081 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11868 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4653 0 3 0 71910 45 0 0 25 0 1 0 1841190092 19832832 4643 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4842 4643 145 145 0 4697 0 [pid=11840] vsize: 19368 Current children cumulated CPU time (s) 719.57 Current children cumulated vsize (Kb) 21492 [startup+730.082 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11868 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4653 0 3 0 72910 45 0 0 25 0 1 0 1841190092 19832832 4643 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 4842 4643 145 145 0 4697 0 [pid=11840] vsize: 19368 Current children cumulated CPU time (s) 729.57 Current children cumulated vsize (Kb) 21492 [startup+740.084 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11868 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4655 0 3 0 73909 45 0 0 25 0 1 0 1841190092 19845120 4645 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4845 4645 145 145 0 4700 0 [pid=11840] vsize: 19380 Current children cumulated CPU time (s) 739.56 Current children cumulated vsize (Kb) 21504 [startup+750.085 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11870 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4668 0 3 0 74909 45 0 0 25 0 1 0 1841190092 19910656 4658 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4861 4658 145 145 0 4716 0 [pid=11840] vsize: 19444 Current children cumulated CPU time (s) 749.56 Current children cumulated vsize (Kb) 21568 [startup+760.086 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11870 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4690 0 3 0 75909 46 0 0 25 0 1 0 1841190092 20008960 4680 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4885 4680 145 145 0 4740 0 [pid=11840] vsize: 19540 Current children cumulated CPU time (s) 759.57 Current children cumulated vsize (Kb) 21664 [startup+770.087 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11870 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4707 0 3 0 76909 46 0 0 25 0 1 0 1841190092 20107264 4697 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4909 4697 145 145 0 4764 0 [pid=11840] vsize: 19636 Current children cumulated CPU time (s) 769.57 Current children cumulated vsize (Kb) 21760 [startup+780.087 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11870 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4712 0 3 0 77909 46 0 0 25 0 1 0 1841190092 20140032 4702 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4917 4702 145 145 0 4772 0 [pid=11840] vsize: 19668 Current children cumulated CPU time (s) 779.57 Current children cumulated vsize (Kb) 21792 [startup+790.088 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11870 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4714 0 3 0 78910 46 0 0 25 0 1 0 1841190092 20140032 4704 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4917 4704 145 145 0 4772 0 [pid=11840] vsize: 19668 Current children cumulated CPU time (s) 789.58 Current children cumulated vsize (Kb) 21792 [startup+800.088 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11870 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4714 0 3 0 79910 46 0 0 25 0 1 0 1841190092 20140032 4704 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4917 4704 145 145 0 4772 0 [pid=11840] vsize: 19668 Current children cumulated CPU time (s) 799.58 Current children cumulated vsize (Kb) 21792 [startup+810.089 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11872 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4715 0 3 0 80909 47 0 0 25 0 1 0 1841190092 20140032 4705 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4917 4705 145 145 0 4772 0 [pid=11840] vsize: 19668 Current children cumulated CPU time (s) 809.58 Current children cumulated vsize (Kb) 21792 [startup+820.09 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11872 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4715 0 3 0 81909 47 0 0 25 0 1 0 1841190092 20140032 4705 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4917 4705 145 145 0 4772 0 [pid=11840] vsize: 19668 Current children cumulated CPU time (s) 819.58 Current children cumulated vsize (Kb) 21792 [startup+830.091 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11872 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4723 0 3 0 82909 48 0 0 25 0 1 0 1841190092 20172800 4713 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4925 4713 145 145 0 4780 0 [pid=11840] vsize: 19700 Current children cumulated CPU time (s) 829.59 Current children cumulated vsize (Kb) 21824 [startup+840.092 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11872 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4723 0 3 0 83909 48 0 0 25 0 1 0 1841190092 20172800 4713 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4925 4713 145 145 0 4780 0 [pid=11840] vsize: 19700 Current children cumulated CPU time (s) 839.59 Current children cumulated vsize (Kb) 21824 [startup+850.093 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11872 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4741 0 3 0 84908 48 0 0 25 0 1 0 1841190092 20303872 4731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4957 4731 145 145 0 4812 0 [pid=11840] vsize: 19828 Current children cumulated CPU time (s) 849.58 Current children cumulated vsize (Kb) 21952 [startup+860.095 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11872 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4742 0 3 0 85909 48 0 0 25 0 1 0 1841190092 20303872 4732 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4957 4732 145 145 0 4812 0 [pid=11840] vsize: 19828 Current children cumulated CPU time (s) 859.59 Current children cumulated vsize (Kb) 21952 [startup+870.096 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11874 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4752 0 3 0 86908 49 0 0 25 0 1 0 1841190092 20336640 4742 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4965 4742 145 145 0 4820 0 [pid=11840] vsize: 19860 Current children cumulated CPU time (s) 869.59 Current children cumulated vsize (Kb) 21984 [startup+880.097 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11874 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4776 0 3 0 87908 49 0 0 25 0 1 0 1841190092 20443136 4766 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 4991 4766 145 145 0 4846 0 [pid=11840] vsize: 19964 Current children cumulated CPU time (s) 879.59 Current children cumulated vsize (Kb) 22088 [startup+890.098 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11874 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4853 0 3 0 88907 50 0 0 25 0 1 0 1841190092 20787200 4843 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5075 4843 145 145 0 4930 0 [pid=11840] vsize: 20300 Current children cumulated CPU time (s) 889.59 Current children cumulated vsize (Kb) 22424 [startup+900.099 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11874 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4880 0 3 0 89907 50 0 0 25 0 1 0 1841190092 20955136 4870 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5116 4870 145 145 0 4971 0 [pid=11840] vsize: 20464 Current children cumulated CPU time (s) 899.59 Current children cumulated vsize (Kb) 22588 [startup+910.101 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11874 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4895 0 3 0 90907 50 0 0 25 0 1 0 1841190092 21053440 4885 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5140 4885 145 145 0 4995 0 [pid=11840] vsize: 20560 Current children cumulated CPU time (s) 909.59 Current children cumulated vsize (Kb) 22684 [startup+920.102 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11874 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4922 0 3 0 91907 50 0 0 25 0 1 0 1841190092 21184512 4912 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5172 4912 145 145 0 5027 0 [pid=11840] vsize: 20688 Current children cumulated CPU time (s) 919.59 Current children cumulated vsize (Kb) 22812 [startup+930.102 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11876 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4935 0 3 0 92907 50 0 0 25 0 1 0 1841190092 21250048 4925 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5188 4925 145 145 0 5043 0 [pid=11840] vsize: 20752 Current children cumulated CPU time (s) 929.59 Current children cumulated vsize (Kb) 22876 [startup+940.103 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11876 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4935 0 3 0 93907 50 0 0 25 0 1 0 1841190092 21250048 4925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5188 4925 145 145 0 5043 0 [pid=11840] vsize: 20752 Current children cumulated CPU time (s) 939.59 Current children cumulated vsize (Kb) 22876 [startup+950.104 s] Raw data (loadavg): 0.99 0.98 0.96 3/58 11876 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4936 0 3 0 94907 51 0 0 25 0 1 0 1841190092 21250048 4926 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5188 4926 145 145 0 5043 0 [pid=11840] vsize: 20752 Current children cumulated CPU time (s) 949.6 Current children cumulated vsize (Kb) 22876 [startup+960.104 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11876 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 4955 0 3 0 95908 51 0 0 25 0 1 0 1841190092 21348352 4945 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5212 4945 145 145 0 5067 0 [pid=11840] vsize: 20848 Current children cumulated CPU time (s) 959.61 Current children cumulated vsize (Kb) 22972 [startup+970.105 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11876 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5037 0 3 0 96906 52 0 0 25 0 1 0 1841190092 21680128 5027 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5293 5027 145 145 0 5148 0 [pid=11840] vsize: 21172 Current children cumulated CPU time (s) 969.6 Current children cumulated vsize (Kb) 23296 [startup+980.106 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11876 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5171 0 3 0 97904 53 0 0 25 0 1 0 1841190092 22224896 5161 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5426 5161 145 145 0 5281 0 [pid=11840] vsize: 21704 Current children cumulated CPU time (s) 979.59 Current children cumulated vsize (Kb) 23828 [startup+990.107 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11878 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5171 0 3 0 98904 53 0 0 25 0 1 0 1841190092 22224896 5161 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5426 5161 145 145 0 5281 0 [pid=11840] vsize: 21704 Current children cumulated CPU time (s) 989.59 Current children cumulated vsize (Kb) 23828 [startup+1000.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11878 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5172 0 3 0 99904 53 0 0 25 0 1 0 1841190092 22224896 5162 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5426 5162 145 145 0 5281 0 [pid=11840] vsize: 21704 Current children cumulated CPU time (s) 999.59 Current children cumulated vsize (Kb) 23828 [startup+1010.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11878 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5256 0 3 0 100903 54 0 0 25 0 1 0 1841190092 22568960 5246 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5510 5246 145 145 0 5365 0 [pid=11840] vsize: 22040 Current children cumulated CPU time (s) 1009.59 Current children cumulated vsize (Kb) 24164 [startup+1020.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11878 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5272 0 3 0 101903 54 0 0 25 0 1 0 1841190092 22638592 5262 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5527 5262 145 145 0 5382 0 [pid=11840] vsize: 22108 Current children cumulated CPU time (s) 1019.59 Current children cumulated vsize (Kb) 24232 [startup+1030.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11878 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5566 0 3 0 102898 56 0 0 25 0 1 0 1841190092 23855104 5556 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 5824 5556 145 145 0 5679 0 [pid=11840] vsize: 23296 Current children cumulated CPU time (s) 1029.56 Current children cumulated vsize (Kb) 25420 [startup+1040.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11878 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 103893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1039.54 Current children cumulated vsize (Kb) 26584 [startup+1050.11 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11880 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 104893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1049.54 Current children cumulated vsize (Kb) 26584 [startup+1060.12 s] Raw data (loadavg): 0.99 0.98 0.96 2/58 11880 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 105893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223024 134551918 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1059.54 Current children cumulated vsize (Kb) 26584 [startup+1070.12 s] Raw data (loadavg): 1.14 1.02 0.97 2/58 11880 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5854 0 3 0 106893 59 0 0 25 0 1 0 1841190092 25047040 5844 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5844 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1069.54 Current children cumulated vsize (Kb) 26584 [startup+1080.12 s] Raw data (loadavg): 1.12 1.02 0.97 2/58 11880 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5855 0 3 0 107894 59 0 0 25 0 1 0 1841190092 25047040 5845 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5845 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1079.55 Current children cumulated vsize (Kb) 26584 [startup+1090.12 s] Raw data (loadavg): 1.10 1.01 0.97 2/58 11880 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5855 0 3 0 108894 60 0 0 25 0 1 0 1841190092 25047040 5845 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5845 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1089.56 Current children cumulated vsize (Kb) 26584 [startup+1100.12 s] Raw data (loadavg): 1.08 1.01 0.97 2/58 11880 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5857 0 3 0 109894 60 0 0 25 0 1 0 1841190092 25047040 5847 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11840/statm): 6115 5847 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1099.56 Current children cumulated vsize (Kb) 26584 [startup+1110.12 s] Raw data (loadavg): 1.07 1.01 0.97 2/58 11882 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 110893 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1109.55 Current children cumulated vsize (Kb) 26584 [startup+1120.12 s] Raw data (loadavg): 1.06 1.01 0.97 2/58 11882 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 111893 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1119.55 Current children cumulated vsize (Kb) 26584 [startup+1130.12 s] Raw data (loadavg): 1.05 1.01 0.97 2/58 11882 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 112894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1129.56 Current children cumulated vsize (Kb) 26584 [startup+1140.12 s] Raw data (loadavg): 1.04 1.01 0.97 2/58 11882 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 113894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1139.56 Current children cumulated vsize (Kb) 26584 [startup+1150.13 s] Raw data (loadavg): 1.04 1.01 0.97 2/58 11882 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 114894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1149.56 Current children cumulated vsize (Kb) 26584 [startup+1160.13 s] Raw data (loadavg): 1.03 1.01 0.97 2/58 11882 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5858 0 3 0 115894 60 0 0 25 0 1 0 1841190092 25047040 5848 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5848 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1159.56 Current children cumulated vsize (Kb) 26584 [startup+1170.13 s] Raw data (loadavg): 1.02 1.01 0.97 2/58 11884 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5862 0 3 0 116894 60 0 0 25 0 1 0 1841190092 25047040 5852 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6115 5852 145 145 0 5970 0 [pid=11840] vsize: 24460 Current children cumulated CPU time (s) 1169.56 Current children cumulated vsize (Kb) 26584 [startup+1180.13 s] Raw data (loadavg): 1.02 1.01 0.97 2/58 11884 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 117894 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0 [pid=11840] vsize: 24520 Current children cumulated CPU time (s) 1179.56 Current children cumulated vsize (Kb) 26644 [startup+1190.13 s] Raw data (loadavg): 1.02 1.00 0.97 2/58 11884 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 118895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0 [pid=11840] vsize: 24520 Current children cumulated CPU time (s) 1189.57 Current children cumulated vsize (Kb) 26644 [startup+1200.13 s] Raw data (loadavg): 1.01 1.00 0.97 2/58 11884 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 119895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0 [pid=11840] vsize: 24520 Current children cumulated CPU time (s) 1199.57 Current children cumulated vsize (Kb) 26644 [startup+1210.13 s] Raw data (loadavg): 1.01 1.00 0.97 2/58 11884 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 120895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0 [pid=11840] vsize: 24520 Current children cumulated CPU time (s) 1209.57 Current children cumulated vsize (Kb) 26644 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 1.01 1.00 0.97 2/58 11884 Raw data (/proc/11836/stat): 11836 (minisat+_script) S 11835 11836 9102 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841190087 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11836/statm): 531 226 485 147 0 384 0 [pid=11836] vsize: 2124 Raw data (/proc/11840/stat): 11840 (minisat+_64-bit) R 11836 11836 9102 0 -1 0 5870 0 3 0 120895 60 0 0 25 0 1 0 1841190092 25108480 5860 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11840/statm): 6130 5860 145 145 0 5985 0 [pid=11840] vsize: 24520 Current children cumulated CPU time (s) 1209.57 Current children cumulated vsize (Kb) 26644 Sending SIGTERM to -11836 Sleeping 2 seconds One traced child (pid=11836) ended because it received signal 15 (SIGTERM) One traced child (pid=11840) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.15 CPU time (s): 1209.58 CPU user time (s): 1208.96 CPU system time (s): 0.618905 CPU usage (%): 99.9529 Max. virtual memory (cumulated for all children) (Kb): 26644
ERROR: no interpretation found !