Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-wood1p.opb |
MD5SUM | ebfeaf296769d76c3baeac85e245b267 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 20 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 1048575 |
Number of bits of the sum of numbers in the objective function | 20 |
Biggest number in a constraint | 52428800000000 |
Number of bits of the biggest number in a constraint | 46 |
Biggest sum of numbers in a constraint | 64856524263290100 |
Number of bits of the biggest sum of numbers | 56 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 51880 |
Total number of constraints | 244 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 244 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 51840 |
LAUNCH ON wulflinc24 THE 2005-09-20 02:59:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3212 boxname=wulflinc24 idbench=868 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ebfeaf296769d76c3baeac85e245b267 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-wood1p.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-wood1p.opb IDLAUNCH: 3212 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 888568 kB Buffers: 4144 kB Cached: 113828 kB SwapCached: 756 kB Active: 50052 kB Inactive: 70480 kB HighTotal: 131008 kB HighFree: 13020 kB LowTotal: 903652 kB LowFree: 875548 kB SwapTotal: 2097892 kB SwapFree: 2096608 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 19728 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:19:23 (client local time) WITH STATUS 0 IN 1199.43 SECONDS stats: 3212 7 1199.43 0
c Parsing PB file... c PARSE ERROR! [line 2719] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead...
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/6187/stat): 6187 (minisat+_script) R 6186 6187 20728 0 -1 0 19 0 0 0 0 0 0 0 25 0 1 0 1855123263 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/6187/statm): 174 3 169 147 0 27 0 [pid=6187] 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=6188 New process pid=6189 New process pid=6190 execve syscall for /bin/sed executable One traced child (pid=6189) 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=6190) exited with status: 0 One traced child (pid=6188) exited with status: 0 New process pid=6191 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-wood1p.opb One traced child (pid=6191) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=6192 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-wood1p.opb [startup+10.0032 s] Raw data (loadavg): 0.95 0.96 0.95 1/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) T 6187 6187 20728 0 -1 0 3613 0 0 0 414 14 0 0 25 0 1 0 1855123817 6443008 1091 4294967295 134512640 135167914 3221224448 3221222540 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6192/statm): 1573 1091 162 162 0 1411 0 [pid=6192] vsize: 6292 Current children cumulated CPU time (s) 9.36 Current children cumulated vsize (Kb) 8420 [startup+20.0039 s] Raw data (loadavg): 0.95 0.96 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 10860 0 0 0 1349 48 0 0 25 0 1 0 1855123817 15847424 2754 4294967295 134512640 135167914 3221224448 3221222828 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 3869 2754 162 162 0 3707 0 [pid=6192] vsize: 15476 Current children cumulated CPU time (s) 19.05 Current children cumulated vsize (Kb) 17604 [startup+30.0056 s] Raw data (loadavg): 0.96 0.96 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 17714 0 0 0 2282 81 0 0 25 0 1 0 1855123817 23789568 3844 4294967295 134512640 135167914 3221224448 3221223200 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 5808 3844 162 162 0 5646 0 [pid=6192] vsize: 23232 Current children cumulated CPU time (s) 28.71 Current children cumulated vsize (Kb) 25360 [startup+40.0063 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 25177 0 0 0 3213 115 0 0 25 0 1 0 1855123817 33730560 5735 4294967295 134512640 135167914 3221224448 3221220500 134611026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 8235 5735 162 162 0 8073 0 [pid=6192] vsize: 32940 Current children cumulated CPU time (s) 38.36 Current children cumulated vsize (Kb) 35068 [startup+50.008 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 32145 0 0 0 4144 147 0 0 25 0 1 0 1855123817 40513536 6733 4294967295 134512640 135167914 3221224448 3221223200 134843404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 9891 6733 162 162 0 9729 0 [pid=6192] vsize: 39564 Current children cumulated CPU time (s) 47.99 Current children cumulated vsize (Kb) 41692 [startup+60.0087 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 39192 0 0 0 5078 181 0 0 25 0 1 0 1855123817 51773440 8423 4294967295 134512640 135167914 3221224448 3221222460 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 12640 8423 162 162 0 12478 0 [pid=6192] vsize: 50560 Current children cumulated CPU time (s) 57.67 Current children cumulated vsize (Kb) 52688 [startup+70.0124 s] Raw data (loadavg): 0.98 0.96 0.95 1/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) T 6187 6187 20728 0 -1 0 46236 0 0 0 6011 212 0 0 25 0 1 0 1855123817 59994112 9850 4294967295 134512640 135167914 3221224448 3221222588 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6192/statm): 14647 9850 162 162 0 14485 0 [pid=6192] vsize: 58588 Current children cumulated CPU time (s) 67.31 Current children cumulated vsize (Kb) 60716 [startup+80.0131 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 52707 0 0 0 6952 239 0 0 25 0 1 0 1855123817 66605056 10835 4294967295 134512640 135167914 3221224448 3221223360 134572109 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 16261 10835 162 162 0 16099 0 [pid=6192] vsize: 65044 Current children cumulated CPU time (s) 76.99 Current children cumulated vsize (Kb) 67172 [startup+90.0138 s] Raw data (loadavg): 0.98 0.96 0.95 1/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) T 6187 6187 20728 0 -1 0 59694 0 0 0 7885 270 0 0 25 0 1 0 1855123817 75235328 12265 4294967295 134512640 135167914 3221224448 3221222556 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6192/statm): 18368 12265 162 162 0 18206 0 [pid=6192] vsize: 73472 Current children cumulated CPU time (s) 86.63 Current children cumulated vsize (Kb) 75600 [startup+100.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 66270 0 0 0 8820 302 0 0 25 0 1 0 1855123817 85708800 14419 4294967295 134512640 135167914 3221224448 3221221248 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 20925 14419 162 162 0 20763 0 [pid=6192] vsize: 83700 Current children cumulated CPU time (s) 96.3 Current children cumulated vsize (Kb) 85828 [startup+110.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 71227 0 0 0 9770 325 0 0 25 0 1 0 1855123817 93212672 15966 4294967295 134512640 135167914 3221224448 3221222224 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 22757 15966 162 162 0 22595 0 [pid=6192] vsize: 91028 Current children cumulated CPU time (s) 106.03 Current children cumulated vsize (Kb) 93156 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 76297 0 0 0 10717 349 0 0 25 0 1 0 1855123817 97951744 16816 4294967295 134512640 135167914 3221224448 3221223280 134849071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 23914 16816 162 162 0 23752 0 [pid=6192] vsize: 95656 Current children cumulated CPU time (s) 115.74 Current children cumulated vsize (Kb) 97784 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 81803 0 0 0 11660 375 0 0 25 0 1 0 1855123817 108265472 19004 4294967295 134512640 135167914 3221224448 3221221296 134516640 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 26432 19004 162 162 0 26270 0 [pid=6192] vsize: 105728 Current children cumulated CPU time (s) 125.43 Current children cumulated vsize (Kb) 107856 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 86246 0 0 0 12614 399 0 0 25 0 1 0 1855123817 114368512 20453 4294967295 134512640 135167914 3221224448 3221222896 134591496 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 27922 20453 162 162 0 27760 0 [pid=6192] vsize: 111688 Current children cumulated CPU time (s) 135.21 Current children cumulated vsize (Kb) 113816 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 91075 0 0 0 13565 422 0 0 25 0 1 0 1855123817 121372672 21847 4294967295 134512640 135167914 3221224448 3221222864 134609905 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 29632 21847 162 162 0 29470 0 [pid=6192] vsize: 118528 Current children cumulated CPU time (s) 144.95 Current children cumulated vsize (Kb) 120656 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.95 1/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) T 6187 6187 20728 0 -1 0 97255 0 0 0 14509 449 0 0 24 0 1 0 1855123817 133079040 24664 4294967295 134512640 135167914 3221224448 3221222556 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6192/statm): 32490 24664 162 162 0 32328 0 [pid=6192] vsize: 129960 Current children cumulated CPU time (s) 154.66 Current children cumulated vsize (Kb) 132088 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 102837 0 0 0 15449 478 0 0 25 0 1 0 1855123817 141787136 26804 4294967295 134512640 135167914 3221224448 3221221232 134695307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6192/statm): 34616 26804 162 162 0 34454 0 [pid=6192] vsize: 138464 Current children cumulated CPU time (s) 164.35 Current children cumulated vsize (Kb) 140592 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106025 0 0 0 16421 491 0 0 25 0 1 0 1855123817 144297984 27467 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27467 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 174.2 Current children cumulated vsize (Kb) 143044 [startup+190.023 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106025 0 0 0 17421 491 0 0 25 0 1 0 1855123817 144297984 27467 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27467 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 184.2 Current children cumulated vsize (Kb) 143044 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106025 0 0 0 18421 492 0 0 25 0 1 0 1855123817 144297984 27467 4294967295 134512640 135167914 3221224448 3221223216 134691327 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27467 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 194.21 Current children cumulated vsize (Kb) 143044 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106025 0 0 0 19421 492 0 0 25 0 1 0 1855123817 144297984 27467 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27467 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 204.21 Current children cumulated vsize (Kb) 143044 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106025 0 0 0 20422 492 0 0 25 0 1 0 1855123817 144297984 27467 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27467 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 214.22 Current children cumulated vsize (Kb) 143044 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106025 0 0 0 21422 492 0 0 25 0 1 0 1855123817 144297984 27467 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27467 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 224.22 Current children cumulated vsize (Kb) 143044 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 22422 492 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223280 134596387 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 234.22 Current children cumulated vsize (Kb) 143044 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 23422 492 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 244.22 Current children cumulated vsize (Kb) 143044 [startup+260.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 24422 492 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223296 134596324 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 254.22 Current children cumulated vsize (Kb) 143044 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 25422 492 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223296 134594196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 264.22 Current children cumulated vsize (Kb) 143044 [startup+280.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 26423 492 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223296 134594194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 274.23 Current children cumulated vsize (Kb) 143044 [startup+290.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 27422 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 284.23 Current children cumulated vsize (Kb) 143044 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 28423 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 294.24 Current children cumulated vsize (Kb) 143044 [startup+310.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 29423 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223216 134691382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 304.24 Current children cumulated vsize (Kb) 143044 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 30423 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 314.24 Current children cumulated vsize (Kb) 143044 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 31423 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223216 134691310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 324.24 Current children cumulated vsize (Kb) 143044 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 32423 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223296 134594165 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 334.24 Current children cumulated vsize (Kb) 143044 [startup+350.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 33423 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 344.24 Current children cumulated vsize (Kb) 143044 [startup+360.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 34424 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 354.25 Current children cumulated vsize (Kb) 143044 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106026 0 0 0 35424 493 0 0 25 0 1 0 1855123817 144297984 27468 4294967295 134512640 135167914 3221224448 3221223276 134691389 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35229 27468 162 162 0 35067 0 [pid=6192] vsize: 140916 Current children cumulated CPU time (s) 364.25 Current children cumulated vsize (Kb) 143044 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 36424 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 374.25 Current children cumulated vsize (Kb) 143048 [startup+390.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 37424 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134594194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 384.25 Current children cumulated vsize (Kb) 143048 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 38424 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134594196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 394.25 Current children cumulated vsize (Kb) 143048 [startup+410.034 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 39424 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 404.25 Current children cumulated vsize (Kb) 143048 [startup+420.035 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 40425 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 414.26 Current children cumulated vsize (Kb) 143048 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 41425 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 424.26 Current children cumulated vsize (Kb) 143048 [startup+440.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 42425 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 434.26 Current children cumulated vsize (Kb) 143048 [startup+450.037 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 43425 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134594196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 444.26 Current children cumulated vsize (Kb) 143048 [startup+460.038 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 44426 493 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134596402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 454.27 Current children cumulated vsize (Kb) 143048 [startup+470.038 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 45425 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 464.27 Current children cumulated vsize (Kb) 143048 [startup+480.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 46426 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 474.28 Current children cumulated vsize (Kb) 143048 [startup+490.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 47426 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691226 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 484.28 Current children cumulated vsize (Kb) 143048 [startup+500.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 48426 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 494.28 Current children cumulated vsize (Kb) 143048 [startup+510.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 49426 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 504.28 Current children cumulated vsize (Kb) 143048 [startup+520.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 50426 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134594245 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 514.28 Current children cumulated vsize (Kb) 143048 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 51427 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 524.29 Current children cumulated vsize (Kb) 143048 [startup+540.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 52427 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223212 134697040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 534.29 Current children cumulated vsize (Kb) 143048 [startup+550.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 53427 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 544.29 Current children cumulated vsize (Kb) 143048 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 54427 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 554.29 Current children cumulated vsize (Kb) 143048 [startup+570.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 55427 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 564.29 Current children cumulated vsize (Kb) 143048 [startup+580.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 56427 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 574.29 Current children cumulated vsize (Kb) 143048 [startup+590.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 57427 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134594196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 584.29 Current children cumulated vsize (Kb) 143048 [startup+600.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 58428 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 594.3 Current children cumulated vsize (Kb) 143048 [startup+610.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 59428 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 604.3 Current children cumulated vsize (Kb) 143048 [startup+620.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 60428 494 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 614.3 Current children cumulated vsize (Kb) 143048 [startup+630.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 61428 495 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223204 134697164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 624.31 Current children cumulated vsize (Kb) 143048 [startup+640.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 62428 495 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 634.31 Current children cumulated vsize (Kb) 143048 [startup+650.045 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 63428 495 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223272 134691201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 644.31 Current children cumulated vsize (Kb) 143048 [startup+660.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 64427 496 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 654.31 Current children cumulated vsize (Kb) 143048 [startup+670.045 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 65427 497 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223296 134596402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 664.32 Current children cumulated vsize (Kb) 143048 [startup+680.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 66427 497 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 674.32 Current children cumulated vsize (Kb) 143048 [startup+690.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 67426 497 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 684.31 Current children cumulated vsize (Kb) 143048 [startup+700.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 68426 498 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691415 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 694.32 Current children cumulated vsize (Kb) 143048 [startup+710.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 69427 498 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 704.33 Current children cumulated vsize (Kb) 143048 [startup+720.048 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 70426 498 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 714.32 Current children cumulated vsize (Kb) 143048 [startup+730.048 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 71427 498 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 724.33 Current children cumulated vsize (Kb) 143048 [startup+740.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 72426 499 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 734.33 Current children cumulated vsize (Kb) 143048 [startup+750.05 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 73427 499 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 744.34 Current children cumulated vsize (Kb) 143048 [startup+760.051 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106027 0 0 0 74427 499 0 0 25 0 1 0 1855123817 144302080 27469 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27469 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 754.34 Current children cumulated vsize (Kb) 143048 [startup+770.05 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 75427 499 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223276 134691200 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 764.34 Current children cumulated vsize (Kb) 143048 [startup+780.051 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 76427 499 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 774.34 Current children cumulated vsize (Kb) 143048 [startup+790.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 77427 499 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 784.34 Current children cumulated vsize (Kb) 143048 [startup+800.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 78427 499 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 794.34 Current children cumulated vsize (Kb) 143048 [startup+810.053 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 79427 499 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697189 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 804.34 Current children cumulated vsize (Kb) 143048 [startup+820.054 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 80427 499 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223264 134522197 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 814.34 Current children cumulated vsize (Kb) 143048 [startup+830.054 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 81428 499 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 824.35 Current children cumulated vsize (Kb) 143048 [startup+840.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 82428 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 834.36 Current children cumulated vsize (Kb) 143048 [startup+850.056 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 83428 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 844.36 Current children cumulated vsize (Kb) 143048 [startup+860.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 84428 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223208 134697041 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 854.36 Current children cumulated vsize (Kb) 143048 [startup+870.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 85428 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223280 134596368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 864.36 Current children cumulated vsize (Kb) 143048 [startup+880.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 86429 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 874.37 Current children cumulated vsize (Kb) 143048 [startup+890.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 87429 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 884.37 Current children cumulated vsize (Kb) 143048 [startup+900.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 88429 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134594254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 894.37 Current children cumulated vsize (Kb) 143048 [startup+910.06 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 89429 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 904.37 Current children cumulated vsize (Kb) 143048 [startup+920.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 90429 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 914.37 Current children cumulated vsize (Kb) 143048 [startup+930.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 91429 500 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 924.37 Current children cumulated vsize (Kb) 143048 [startup+940.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 92429 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691231 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 934.38 Current children cumulated vsize (Kb) 143048 [startup+950.062 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 93429 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 944.38 Current children cumulated vsize (Kb) 143048 [startup+960.062 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 94430 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691316 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 954.39 Current children cumulated vsize (Kb) 143048 [startup+970.062 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 95430 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 964.39 Current children cumulated vsize (Kb) 143048 [startup+980.063 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 96430 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 974.39 Current children cumulated vsize (Kb) 143048 [startup+990.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 97430 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134594194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 984.39 Current children cumulated vsize (Kb) 143048 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 98430 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 994.39 Current children cumulated vsize (Kb) 143048 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 99430 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1004.39 Current children cumulated vsize (Kb) 143048 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 100431 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1014.4 Current children cumulated vsize (Kb) 143048 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 101431 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1024.4 Current children cumulated vsize (Kb) 143048 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 102431 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1034.4 Current children cumulated vsize (Kb) 143048 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 103431 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1044.4 Current children cumulated vsize (Kb) 143048 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 104432 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223280 134596373 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1054.41 Current children cumulated vsize (Kb) 143048 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 105432 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223276 134691389 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1064.41 Current children cumulated vsize (Kb) 143048 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 106432 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1074.41 Current children cumulated vsize (Kb) 143048 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 107432 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134594194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1084.41 Current children cumulated vsize (Kb) 143048 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 108432 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1094.41 Current children cumulated vsize (Kb) 143048 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 109432 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1104.41 Current children cumulated vsize (Kb) 143048 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 110433 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1114.42 Current children cumulated vsize (Kb) 143048 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 111433 501 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1124.42 Current children cumulated vsize (Kb) 143048 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 112433 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1134.43 Current children cumulated vsize (Kb) 143048 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 113433 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1144.43 Current children cumulated vsize (Kb) 143048 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 114433 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1154.43 Current children cumulated vsize (Kb) 143048 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 115433 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1164.43 Current children cumulated vsize (Kb) 143048 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 116434 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1174.44 Current children cumulated vsize (Kb) 143048 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 117434 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134596324 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1184.44 Current children cumulated vsize (Kb) 143048 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 118434 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134594254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1194.44 Current children cumulated vsize (Kb) 143048 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 119434 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1204.44 Current children cumulated vsize (Kb) 143048 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 6192 Raw data (/proc/6187/stat): 6187 (minisat+_script) S 6186 6187 20728 0 -1 0 314 12790 0 0 0 1 453 54 18 0 1 0 1855123263 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6187/statm): 532 234 485 147 0 385 0 [pid=6187] vsize: 2128 Raw data (/proc/6192/stat): 6192 (minisat+_bignum) R 6187 6187 20728 0 -1 0 106028 0 0 0 119435 502 0 0 25 0 1 0 1855123817 144302080 27470 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6192/statm): 35230 27470 162 162 0 35068 0 [pid=6192] vsize: 140920 Current children cumulated CPU time (s) 1204.45 Current children cumulated vsize (Kb) 143048 Sending SIGTERM to -6187 Sleeping 2 seconds One traced child (pid=6187) ended because it received signal 15 (SIGTERM) One traced child (pid=6192) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1199.43 CPU user time (s): 1194.35 CPU system time (s): 5.07523 CPU usage (%): 99.1151 Max. virtual memory (cumulated for all children) (Kb): 143048
ERROR: no interpretation found !