Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-boeing2.opb |
MD5SUM | 9d4981de84e8fd488c4493c292301fa3 |
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 | 3114 |
Biggest coefficient in the objective function | 40265318400000 |
Number of bits for the biggest coefficient in the objective function | 46 |
Sum of the numbers in the objective function | 2533036563346675 |
Number of bits of the sum of numbers in the objective function | 52 |
Biggest number in a constraint | 431563682611200 |
Number of bits of the biggest number in a constraint | 49 |
Biggest sum of numbers in a constraint | 17042207919312540 |
Number of bits of the biggest sum of numbers | 54 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 3371 |
Total number of constraints | 213 |
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 | 213 |
Minimum length of a constraint | 12 |
Maximum length of a constraint | 2370 |
LAUNCH ON wulflinc3 THE 2005-09-18 20:39:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2832 boxname=wulflinc3 idbench=488 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9d4981de84e8fd488c4493c292301fa3 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-boeing2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-boeing2.opb IDLAUNCH: 2832 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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: 925096 kB Buffers: 34504 kB Cached: 48756 kB SwapCached: 856 kB Active: 64304 kB Inactive: 21612 kB HighTotal: 131008 kB HighFree: 80724 kB LowTotal: 903652 kB LowFree: 844372 kB SwapTotal: 2097136 kB SwapFree: 2095712 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5720 kB Slab: 18028 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 21:00:02 (client local time) WITH STATUS 0 IN 1205.28 SECONDS stats: 2832 7 1205.28 0
c Parsing PB file... c PARSE ERROR! [line 258] 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/20941/stat): 20941 (minisat+_script) R 20940 20941 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785965617 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/20941/statm): 174 3 169 147 0 27 0 [pid=20941] 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=20942 New process pid=20943 New process pid=20944 execve syscall for /bin/sed executable One traced child (pid=20943) 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=20944) exited with status: 0 One traced child (pid=20942) exited with status: 0 New process pid=20945 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-boeing2.opb One traced child (pid=20945) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=20946 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-boeing2.opb [startup+10.0034 s] Raw data (loadavg): 0.97 0.96 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 4700 0 0 0 944 20 0 0 25 0 1 0 1785965633 16670720 3902 4294967295 134512640 135167914 3221224448 3221199712 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 4070 3902 162 162 0 3908 0 [pid=20946] vsize: 16280 Current children cumulated CPU time (s) 9.75 Current children cumulated vsize (Kb) 18408 [startup+20.0053 s] Raw data (loadavg): 0.97 0.96 0.93 1/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) T 20941 20941 31915 0 -1 0 10317 0 0 0 1889 46 0 0 25 0 1 0 1785965633 36978688 8860 4294967295 134512640 135167914 3221224448 3221199804 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/20946/statm): 9028 8860 162 162 0 8866 0 [pid=20946] vsize: 36112 Current children cumulated CPU time (s) 19.46 Current children cumulated vsize (Kb) 38240 [startup+30.0061 s] Raw data (loadavg): 0.98 0.96 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 16842 0 0 0 2839 70 0 0 25 0 1 0 1785965633 58306560 14067 4294967295 134512640 135167914 3221224448 3221199740 134694368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 14235 14067 162 162 0 14073 0 [pid=20946] vsize: 56940 Current children cumulated CPU time (s) 29.2 Current children cumulated vsize (Kb) 59068 [startup+40.0059 s] Raw data (loadavg): 0.98 0.96 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 21008 0 0 0 3795 90 0 0 25 0 1 0 1785965633 75370496 18233 4294967295 134512640 135167914 3221224448 3221200636 134624320 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 18401 18233 162 162 0 18239 0 [pid=20946] vsize: 73604 Current children cumulated CPU time (s) 38.96 Current children cumulated vsize (Kb) 75732 [startup+50.0068 s] Raw data (loadavg): 0.98 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 29492 0 0 0 4750 115 0 0 25 0 1 0 1785965633 99315712 24080 4294967295 134512640 135167914 3221224448 3221199328 134845130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 24247 24080 162 162 0 24085 0 [pid=20946] vsize: 96988 Current children cumulated CPU time (s) 48.76 Current children cumulated vsize (Kb) 99116 [startup+60.0076 s] Raw data (loadavg): 0.98 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 33507 0 0 0 5703 133 0 0 25 0 1 0 1785965633 115757056 28095 4294967295 134512640 135167914 3221224448 3221199908 134844636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 28261 28095 162 162 0 28099 0 [pid=20946] vsize: 113044 Current children cumulated CPU time (s) 58.47 Current children cumulated vsize (Kb) 115172 [startup+70.0094 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 37353 0 0 0 6658 152 0 0 25 0 1 0 1785965633 131510272 31941 4294967295 134512640 135167914 3221224448 3221200752 134845933 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 32107 31941 162 162 0 31945 0 [pid=20946] vsize: 128428 Current children cumulated CPU time (s) 68.21 Current children cumulated vsize (Kb) 130556 [startup+80.0103 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 41060 0 0 0 7619 167 0 0 25 0 1 0 1785965633 146690048 35648 4294967295 134512640 135167914 3221224448 3221200752 134624952 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 35813 35648 162 162 0 35651 0 [pid=20946] vsize: 143252 Current children cumulated CPU time (s) 77.97 Current children cumulated vsize (Kb) 145380 [startup+90.0101 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 53970 0 0 0 8572 200 0 0 25 0 1 0 1785965633 199569408 48558 4294967295 134512640 135167914 3221224448 3221201936 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 48723 48558 162 162 0 48561 0 [pid=20946] vsize: 194892 Current children cumulated CPU time (s) 87.83 Current children cumulated vsize (Kb) 197020 [startup+100.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 57141 0 0 0 9534 216 0 0 25 0 1 0 1785965633 190959616 46456 4294967295 134512640 135167914 3221224448 3221202536 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 46621 46456 162 162 0 46459 0 [pid=20946] vsize: 186484 Current children cumulated CPU time (s) 97.61 Current children cumulated vsize (Kb) 188612 [startup+110.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 60738 0 0 0 10495 233 0 0 25 0 1 0 1785965633 205692928 50053 4294967295 134512640 135167914 3221224448 3221199680 134696152 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 50218 50053 162 162 0 50056 0 [pid=20946] vsize: 200872 Current children cumulated CPU time (s) 107.39 Current children cumulated vsize (Kb) 203000 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 64342 0 0 0 11459 247 0 0 25 0 1 0 1785965633 220454912 53657 4294967295 134512640 135167914 3221224448 3221200044 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 53822 53657 162 162 0 53660 0 [pid=20946] vsize: 215288 Current children cumulated CPU time (s) 117.17 Current children cumulated vsize (Kb) 217416 [startup+130.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 68012 0 0 0 12419 261 0 0 25 0 1 0 1785965633 235487232 57327 4294967295 134512640 135167914 3221224448 3221201280 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 57492 57327 162 162 0 57330 0 [pid=20946] vsize: 229968 Current children cumulated CPU time (s) 126.91 Current children cumulated vsize (Kb) 232096 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 71576 0 0 0 13382 274 0 0 25 0 1 0 1785965633 250081280 60891 4294967295 134512640 135167914 3221224448 3221200848 134849066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 61055 60891 162 162 0 60893 0 [pid=20946] vsize: 244220 Current children cumulated CPU time (s) 136.67 Current children cumulated vsize (Kb) 246348 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 75024 0 0 0 14346 289 0 0 25 0 1 0 1785965633 264204288 64339 4294967295 134512640 135167914 3221224448 3221201344 134844715 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 64503 64339 162 162 0 64341 0 [pid=20946] vsize: 258012 Current children cumulated CPU time (s) 146.46 Current children cumulated vsize (Kb) 260140 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 78461 0 0 0 15311 304 0 0 25 0 1 0 1785965633 278282240 67776 4294967295 134512640 135167914 3221224448 3221200088 134842997 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 67940 67776 162 162 0 67778 0 [pid=20946] vsize: 271760 Current children cumulated CPU time (s) 156.26 Current children cumulated vsize (Kb) 273888 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 81932 0 0 0 16271 321 0 0 25 0 1 0 1785965633 292499456 71247 4294967295 134512640 135167914 3221224448 3221201056 134694407 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 71411 71247 162 162 0 71249 0 [pid=20946] vsize: 285644 Current children cumulated CPU time (s) 166.03 Current children cumulated vsize (Kb) 287772 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.93 1/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) T 20941 20941 31915 0 -1 0 85356 0 0 0 17235 336 0 0 25 0 1 0 1785965633 306520064 74671 4294967295 134512640 135167914 3221224448 3221199276 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/20946/statm): 74834 74671 162 162 0 74672 0 [pid=20946] vsize: 299336 Current children cumulated CPU time (s) 175.82 Current children cumulated vsize (Kb) 301464 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 106868 0 0 0 18183 385 0 0 25 0 1 0 1785965633 351436800 85637 4294967295 134512640 135167914 3221224448 3221200064 134843426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 85800 85637 162 162 0 85638 0 [pid=20946] vsize: 343200 Current children cumulated CPU time (s) 185.79 Current children cumulated vsize (Kb) 345328 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) T 20941 20941 31915 0 -1 0 110143 0 0 0 19149 399 0 0 25 0 1 0 1785965633 364851200 88912 4294967295 134512640 135167914 3221224448 3221199708 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/20946/statm): 89075 88912 162 162 0 88913 0 [pid=20946] vsize: 356300 Current children cumulated CPU time (s) 195.59 Current children cumulated vsize (Kb) 358428 [startup+210.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 113555 0 0 0 20115 413 0 0 25 0 1 0 1785965633 378822656 92324 4294967295 134512640 135167914 3221224448 3221200000 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 92486 92324 162 162 0 92324 0 [pid=20946] vsize: 369944 Current children cumulated CPU time (s) 205.39 Current children cumulated vsize (Kb) 372072 [startup+220.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 116814 0 0 0 21081 426 0 0 25 0 1 0 1785965633 392167424 95583 4294967295 134512640 135167914 3221224448 3221200820 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 95744 95583 162 162 0 95582 0 [pid=20946] vsize: 382976 Current children cumulated CPU time (s) 215.18 Current children cumulated vsize (Kb) 385104 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 22060 433 0 0 25 0 1 0 1785965633 400191488 97542 4294967295 134512640 135167914 3221224448 3221223200 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 97703 97542 162 162 0 97541 0 [pid=20946] vsize: 390812 Current children cumulated CPU time (s) 225.04 Current children cumulated vsize (Kb) 392940 [startup+240.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 23056 437 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221218656 134629049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 235.04 Current children cumulated vsize (Kb) 308576 [startup+250.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 24056 437 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219164 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 245.04 Current children cumulated vsize (Kb) 308576 [startup+260.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 25056 438 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219280 134696200 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 255.05 Current children cumulated vsize (Kb) 308576 [startup+270.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 26056 438 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219344 134849066 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 265.05 Current children cumulated vsize (Kb) 308576 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 27056 438 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221218908 134844675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 275.05 Current children cumulated vsize (Kb) 308576 [startup+290.025 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 28055 439 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219668 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 285.05 Current children cumulated vsize (Kb) 308576 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 29055 439 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221218988 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 295.05 Current children cumulated vsize (Kb) 308576 [startup+310.025 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 30055 439 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219100 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 305.05 Current children cumulated vsize (Kb) 308576 [startup+320.026 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 31055 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220352 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 315.06 Current children cumulated vsize (Kb) 308576 [startup+330.027 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 32055 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220000 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 325.06 Current children cumulated vsize (Kb) 308576 [startup+340.028 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 33055 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219484 134845882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 335.06 Current children cumulated vsize (Kb) 308576 [startup+350.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 34054 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220032 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 345.05 Current children cumulated vsize (Kb) 308576 [startup+360.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 35054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219284 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 355.06 Current children cumulated vsize (Kb) 308576 [startup+370.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 36054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219856 134694545 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 365.06 Current children cumulated vsize (Kb) 308576 [startup+380.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 37054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220384 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 375.06 Current children cumulated vsize (Kb) 308576 [startup+390.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 38054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220720 134522355 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 385.06 Current children cumulated vsize (Kb) 308576 [startup+400.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 39054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220032 134694517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 395.06 Current children cumulated vsize (Kb) 308576 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 40054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220012 134844675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 405.06 Current children cumulated vsize (Kb) 308576 [startup+420.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 41054 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219552 134844708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 415.07 Current children cumulated vsize (Kb) 308576 [startup+430.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 42053 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219120 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 425.06 Current children cumulated vsize (Kb) 308576 [startup+440.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 43053 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134843074 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 435.06 Current children cumulated vsize (Kb) 308576 [startup+450.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 44053 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220608 134629448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 445.06 Current children cumulated vsize (Kb) 308576 [startup+460.035 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 45053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219540 134630869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 455.07 Current children cumulated vsize (Kb) 308576 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 46053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219792 134843012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 465.07 Current children cumulated vsize (Kb) 308576 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 47053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219984 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 475.07 Current children cumulated vsize (Kb) 308576 [startup+490.037 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 48053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220504 134693686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 485.07 Current children cumulated vsize (Kb) 308576 [startup+500.037 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 49053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219696 134696407 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 495.07 Current children cumulated vsize (Kb) 308576 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 50052 444 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220560 134849099 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 505.07 Current children cumulated vsize (Kb) 308576 [startup+520.039 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 51052 444 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220432 134629448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 515.07 Current children cumulated vsize (Kb) 308576 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 52052 444 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220496 134696781 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 525.07 Current children cumulated vsize (Kb) 308576 [startup+540.041 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 53051 446 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220236 134522361 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 535.08 Current children cumulated vsize (Kb) 308576 [startup+550.042 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 54050 447 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219324 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 545.08 Current children cumulated vsize (Kb) 308576 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 55050 447 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220320 134845901 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 555.08 Current children cumulated vsize (Kb) 308576 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 56049 447 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220160 134843001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 565.07 Current children cumulated vsize (Kb) 308576 [startup+580.045 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 57049 448 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220400 134693582 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 575.08 Current children cumulated vsize (Kb) 308576 [startup+590.045 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 58048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220320 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 585.08 Current children cumulated vsize (Kb) 308576 [startup+600.046 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 59048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220176 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 595.08 Current children cumulated vsize (Kb) 308576 [startup+610.047 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 60048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219264 134844736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 605.08 Current children cumulated vsize (Kb) 308576 [startup+620.047 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 61048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220420 134629088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 615.08 Current children cumulated vsize (Kb) 308576 [startup+630.048 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 62048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220760 134522185 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 625.08 Current children cumulated vsize (Kb) 308576 [startup+640.049 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 63049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219504 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 635.09 Current children cumulated vsize (Kb) 308576 [startup+650.05 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 64049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219528 134693815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 645.09 Current children cumulated vsize (Kb) 308576 [startup+660.051 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 65049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219352 134693744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 655.09 Current children cumulated vsize (Kb) 308576 [startup+670.052 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 66049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219116 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 665.09 Current children cumulated vsize (Kb) 308576 [startup+680.052 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 67050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220484 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 675.1 Current children cumulated vsize (Kb) 308576 [startup+690.053 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 68050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219540 134630852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 685.1 Current children cumulated vsize (Kb) 308576 [startup+700.054 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 69050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220784 134844725 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 695.1 Current children cumulated vsize (Kb) 308576 [startup+710.055 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 70050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220496 134844691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 705.1 Current children cumulated vsize (Kb) 308576 [startup+720.056 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 71050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221424 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 715.1 Current children cumulated vsize (Kb) 308576 [startup+730.057 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 72051 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219616 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 725.11 Current children cumulated vsize (Kb) 308576 [startup+740.057 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 73051 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220304 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 735.11 Current children cumulated vsize (Kb) 308576 [startup+750.058 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 74051 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220592 134629224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 745.12 Current children cumulated vsize (Kb) 308576 [startup+760.059 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 75051 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 755.12 Current children cumulated vsize (Kb) 308576 [startup+770.06 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 76052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844725 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 765.13 Current children cumulated vsize (Kb) 308576 [startup+780.061 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 77052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844725 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 775.13 Current children cumulated vsize (Kb) 308576 [startup+790.061 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 78052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220040 134722513 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 785.13 Current children cumulated vsize (Kb) 308576 [startup+800.061 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 79052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219824 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 795.13 Current children cumulated vsize (Kb) 308576 [startup+810.062 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 80053 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220384 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 805.14 Current children cumulated vsize (Kb) 308576 [startup+820.064 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 81053 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220304 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 815.14 Current children cumulated vsize (Kb) 308576 [startup+830.065 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 82054 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220360 134844633 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 825.15 Current children cumulated vsize (Kb) 308576 [startup+840.074 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 83054 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220236 134694320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 835.15 Current children cumulated vsize (Kb) 308576 [startup+850.075 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 84055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220760 134693815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 845.16 Current children cumulated vsize (Kb) 308576 [startup+860.075 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 85055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220768 134629290 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 855.16 Current children cumulated vsize (Kb) 308576 [startup+870.076 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 86055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220560 134843074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 865.16 Current children cumulated vsize (Kb) 308576 [startup+880.077 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 87055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 875.16 Current children cumulated vsize (Kb) 308576 [startup+890.078 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 88056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 885.17 Current children cumulated vsize (Kb) 308576 [startup+900.079 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 89056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220412 134694320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 895.17 Current children cumulated vsize (Kb) 308576 [startup+910.08 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 90056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220608 134629024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 905.17 Current children cumulated vsize (Kb) 308576 [startup+920.08 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 91056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219756 134844638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 915.17 Current children cumulated vsize (Kb) 308576 [startup+930.081 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 92057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219296 134844637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 925.18 Current children cumulated vsize (Kb) 308576 [startup+940.082 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 93057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220208 134694524 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 935.18 Current children cumulated vsize (Kb) 308576 [startup+950.083 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 94057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219888 134629345 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 945.18 Current children cumulated vsize (Kb) 308576 [startup+960.084 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 95057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221136 134629382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 955.18 Current children cumulated vsize (Kb) 308576 [startup+970.085 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 96057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220948 134630852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 965.18 Current children cumulated vsize (Kb) 308576 [startup+980.085 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 97058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221632 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 975.19 Current children cumulated vsize (Kb) 308576 [startup+990.086 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 98058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219968 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 985.19 Current children cumulated vsize (Kb) 308576 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 99058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220144 134696353 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 995.19 Current children cumulated vsize (Kb) 308576 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 100058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219980 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1005.19 Current children cumulated vsize (Kb) 308576 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 101059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220320 134844736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1015.2 Current children cumulated vsize (Kb) 308576 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 102059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220496 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1025.2 Current children cumulated vsize (Kb) 308576 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 103059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220432 134630728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1035.2 Current children cumulated vsize (Kb) 308576 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 104059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219440 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1045.2 Current children cumulated vsize (Kb) 308576 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 105060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220412 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1055.21 Current children cumulated vsize (Kb) 308576 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 106060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220480 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1065.21 Current children cumulated vsize (Kb) 308576 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 107060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219680 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1075.21 Current children cumulated vsize (Kb) 308576 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 108060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134843139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1085.21 Current children cumulated vsize (Kb) 308576 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 109060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219872 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1095.21 Current children cumulated vsize (Kb) 308576 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 110060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220764 134696560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1105.21 Current children cumulated vsize (Kb) 308576 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 111061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220928 134849066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1115.22 Current children cumulated vsize (Kb) 308576 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 112061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219984 134696578 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1125.22 Current children cumulated vsize (Kb) 308576 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 113061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220144 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1135.22 Current children cumulated vsize (Kb) 308576 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 114061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220848 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1145.22 Current children cumulated vsize (Kb) 308576 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 115062 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220692 134843000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1155.23 Current children cumulated vsize (Kb) 308576 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 116062 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220080 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1165.23 Current children cumulated vsize (Kb) 308576 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 117062 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219072 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1175.23 Current children cumulated vsize (Kb) 308576 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 118063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221024 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1185.24 Current children cumulated vsize (Kb) 308576 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.93 3/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 119063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220864 134696653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1195.24 Current children cumulated vsize (Kb) 308576 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 120063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220948 134628664 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1205.24 Current children cumulated vsize (Kb) 308576 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 20946 Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/20941/statm): 532 234 485 147 0 385 0 [pid=20941] vsize: 2128 Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 120063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220888 134845939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0 [pid=20946] vsize: 306448 Current children cumulated CPU time (s) 1205.24 Current children cumulated vsize (Kb) 308576 Sending SIGTERM to -20941 Sleeping 2 seconds One traced child (pid=20941) ended because it received signal 15 (SIGTERM) One traced child (pid=20946) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.25 CPU time (s): 1205.28 CPU user time (s): 1200.64 CPU system time (s): 4.64129 CPU usage (%): 99.5891 Max. virtual memory (cumulated for all children) (Kb): 392940
ERROR: no interpretation found !