Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-agg3.opb |
MD5SUM | 39aa57894e5a2a46514193d566bffe40 |
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 | 6930 |
Biggest coefficient in the objective function | 53730040872960 |
Number of bits for the biggest coefficient in the objective function | 46 |
Sum of the numbers in the objective function | 8516865379203027 |
Number of bits of the sum of numbers in the objective function | 53 |
Biggest number in a constraint | 22763326668800000 |
Number of bits of the biggest number in a constraint | 55 |
Biggest sum of numbers in a constraint | 46271983665442689 |
Number of bits of the biggest sum of numbers | 56 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 9060 |
Total number of constraints | 467 |
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 | 467 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 1440 |
LAUNCH ON wulflinc25 THE 2005-09-18 20:09:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2751 boxname=wulflinc25 idbench=407 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 39aa57894e5a2a46514193d566bffe40 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-agg3.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-agg3.opb IDLAUNCH: 2751 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 901736 kB Buffers: 35544 kB Cached: 69980 kB SwapCached: 896 kB Active: 69412 kB Inactive: 38732 kB HighTotal: 131008 kB HighFree: 59668 kB LowTotal: 903652 kB LowFree: 842068 kB SwapTotal: 2097892 kB SwapFree: 2096496 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 19200 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:29:31 (client local time) WITH STATUS 0 IN 1209.77 SECONDS stats: 2751 7 1209.77 0
c Parsing PB file... c PARSE ERROR! [line 306] 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/16076/stat): 16076 (minisat+_script) R 16075 16076 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1844048988 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/16076/statm): 174 3 169 147 0 27 0 [pid=16076] 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=16077 New process pid=16078 New process pid=16079 execve syscall for /bin/sed executable 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 One traced child (pid=16078) exited with status: 0 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=16079) exited with status: 0 One traced child (pid=16077) exited with status: 0 New process pid=16080 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-agg3.opb One traced child (pid=16080) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=16081 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-agg3.opb [startup+10.0044 s] Raw data (loadavg): 0.52 0.79 0.88 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 1996 0 3 0 947 14 0 0 25 0 1 0 1844048995 8712192 1931 4294967295 134512640 135167914 3221224448 3221220860 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2127 1931 162 162 0 1965 0 [pid=16081] vsize: 8508 Current children cumulated CPU time (s) 9.62 Current children cumulated vsize (Kb) 10636 [startup+20.005 s] Raw data (loadavg): 0.60 0.79 0.88 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2053 0 3 0 1946 15 0 0 25 0 1 0 1844048995 8896512 1988 4294967295 134512640 135167914 3221224448 3221220144 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2172 1988 162 162 0 2010 0 [pid=16081] vsize: 8688 Current children cumulated CPU time (s) 19.62 Current children cumulated vsize (Kb) 10816 [startup+30.0056 s] Raw data (loadavg): 0.66 0.80 0.88 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2053 0 3 0 2946 15 0 0 25 0 1 0 1844048995 8896512 1988 4294967295 134512640 135167914 3221224448 3221221504 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2172 1988 162 162 0 2010 0 [pid=16081] vsize: 8688 Current children cumulated CPU time (s) 29.62 Current children cumulated vsize (Kb) 10816 [startup+40.0062 s] Raw data (loadavg): 0.71 0.81 0.88 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2183 0 3 0 3945 16 0 0 25 0 1 0 1844048995 9347072 2076 4294967295 134512640 135167914 3221224448 3221218660 134629088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2282 2076 162 162 0 2120 0 [pid=16081] vsize: 9128 Current children cumulated CPU time (s) 39.62 Current children cumulated vsize (Kb) 11256 [startup+50.0068 s] Raw data (loadavg): 0.75 0.81 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2183 0 3 0 4945 16 0 0 25 0 1 0 1844048995 9347072 2076 4294967295 134512640 135167914 3221224448 3221220068 134629088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2282 2076 162 162 0 2120 0 [pid=16081] vsize: 9128 Current children cumulated CPU time (s) 49.62 Current children cumulated vsize (Kb) 11256 [startup+60.0074 s] Raw data (loadavg): 0.79 0.82 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2183 0 3 0 5945 16 0 0 25 0 1 0 1844048995 9347072 2076 4294967295 134512640 135167914 3221224448 3221220384 134843026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2282 2076 162 162 0 2120 0 [pid=16081] vsize: 9128 Current children cumulated CPU time (s) 59.62 Current children cumulated vsize (Kb) 11256 [startup+70.009 s] Raw data (loadavg): 0.82 0.82 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2183 0 3 0 6945 16 0 0 25 0 1 0 1844048995 9347072 2076 4294967295 134512640 135167914 3221224448 3221220560 134694396 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2282 2076 162 162 0 2120 0 [pid=16081] vsize: 9128 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 11256 [startup+80.0096 s] Raw data (loadavg): 0.85 0.83 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2183 0 3 0 7944 17 0 0 25 0 1 0 1844048995 9347072 2076 4294967295 134512640 135167914 3221224448 3221221580 134845882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2282 2076 162 162 0 2120 0 [pid=16081] vsize: 9128 Current children cumulated CPU time (s) 79.62 Current children cumulated vsize (Kb) 11256 [startup+90.0102 s] Raw data (loadavg): 0.87 0.83 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2183 0 3 0 8944 17 0 0 25 0 1 0 1844048995 9347072 2076 4294967295 134512640 135167914 3221224448 3221221644 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2282 2076 162 162 0 2120 0 [pid=16081] vsize: 9128 Current children cumulated CPU time (s) 89.62 Current children cumulated vsize (Kb) 11256 [startup+100.011 s] Raw data (loadavg): 0.89 0.84 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2183 0 3 0 9944 17 0 0 25 0 1 0 1844048995 9347072 2076 4294967295 134512640 135167914 3221224448 3221221820 134694551 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2282 2076 162 162 0 2120 0 [pid=16081] vsize: 9128 Current children cumulated CPU time (s) 99.62 Current children cumulated vsize (Kb) 11256 [startup+110.011 s] Raw data (loadavg): 0.91 0.84 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 10943 18 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221218960 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 109.62 Current children cumulated vsize (Kb) 11504 [startup+120.012 s] Raw data (loadavg): 0.92 0.85 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 11943 18 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220432 134844689 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 119.62 Current children cumulated vsize (Kb) 11504 [startup+130.013 s] Raw data (loadavg): 0.93 0.85 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 12943 18 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221608 134845877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 129.62 Current children cumulated vsize (Kb) 11504 [startup+140.013 s] Raw data (loadavg): 0.94 0.86 0.89 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 13942 19 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221296 134629353 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 139.62 Current children cumulated vsize (Kb) 11504 [startup+150.014 s] Raw data (loadavg): 0.95 0.86 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 14942 19 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221218320 134844703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 149.62 Current children cumulated vsize (Kb) 11504 [startup+160.015 s] Raw data (loadavg): 0.96 0.86 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 15942 20 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221218912 134696376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 159.63 Current children cumulated vsize (Kb) 11504 [startup+170.016 s] Raw data (loadavg): 0.96 0.87 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 16942 20 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221219324 134722542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 169.63 Current children cumulated vsize (Kb) 11504 [startup+180.016 s] Raw data (loadavg): 0.97 0.87 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 17941 20 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221219904 134629001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 11504 [startup+190.017 s] Raw data (loadavg): 0.97 0.88 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 18941 21 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221219820 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 189.63 Current children cumulated vsize (Kb) 11504 [startup+200.017 s] Raw data (loadavg): 0.98 0.88 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 19941 21 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221219700 134696408 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 199.63 Current children cumulated vsize (Kb) 11504 [startup+210.017 s] Raw data (loadavg): 0.98 0.88 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 20941 21 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221219504 134843420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 209.63 Current children cumulated vsize (Kb) 11504 [startup+220.018 s] Raw data (loadavg): 0.98 0.89 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 21940 22 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220400 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 219.63 Current children cumulated vsize (Kb) 11504 [startup+230.018 s] Raw data (loadavg): 0.98 0.89 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 22940 22 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221219968 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 229.63 Current children cumulated vsize (Kb) 11504 [startup+240.018 s] Raw data (loadavg): 0.99 0.89 0.90 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 23940 22 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220032 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 239.63 Current children cumulated vsize (Kb) 11504 [startup+250.019 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 24940 23 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220416 134629340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 249.64 Current children cumulated vsize (Kb) 11504 [startup+260.019 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 25940 23 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220116 134844636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 259.64 Current children cumulated vsize (Kb) 11504 [startup+270.02 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 26940 23 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220540 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 269.64 Current children cumulated vsize (Kb) 11504 [startup+280.021 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 27940 23 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 279.64 Current children cumulated vsize (Kb) 11504 [startup+290.021 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 28939 24 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220688 134696205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 289.64 Current children cumulated vsize (Kb) 11504 [startup+300.022 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 29939 24 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220256 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 299.64 Current children cumulated vsize (Kb) 11504 [startup+310.023 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 30939 24 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 309.64 Current children cumulated vsize (Kb) 11504 [startup+320.024 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 31940 24 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220552 134695249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 319.65 Current children cumulated vsize (Kb) 11504 [startup+330.024 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 32939 24 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220672 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 329.64 Current children cumulated vsize (Kb) 11504 [startup+340.024 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 33939 24 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221376 134845890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 339.64 Current children cumulated vsize (Kb) 11504 [startup+350.025 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 34939 24 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221728 134844694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 349.64 Current children cumulated vsize (Kb) 11504 [startup+360.025 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 35939 25 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220860 134723267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 359.65 Current children cumulated vsize (Kb) 11504 [startup+370.026 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 36939 25 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220848 134844736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 369.65 Current children cumulated vsize (Kb) 11504 [startup+380.026 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 37939 25 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221376 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 379.65 Current children cumulated vsize (Kb) 11504 [startup+390.026 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 38939 25 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221220648 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 389.65 Current children cumulated vsize (Kb) 11504 [startup+400.027 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 39937 27 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 399.65 Current children cumulated vsize (Kb) 11504 [startup+410.027 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 40936 28 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221440 134522310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 409.65 Current children cumulated vsize (Kb) 11504 [startup+420.028 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 41935 29 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221440 134522737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 419.65 Current children cumulated vsize (Kb) 11504 [startup+430.029 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 42935 30 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221468 134694367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 429.66 Current children cumulated vsize (Kb) 11504 [startup+440.029 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 43934 30 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221904 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 439.65 Current children cumulated vsize (Kb) 11504 [startup+450.03 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 44934 31 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221792 134843015 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 449.66 Current children cumulated vsize (Kb) 11504 [startup+460.031 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 45934 31 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221056 134722532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 459.66 Current children cumulated vsize (Kb) 11504 [startup+470.032 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 46934 31 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221200 134845933 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 469.66 Current children cumulated vsize (Kb) 11504 [startup+480.032 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 47933 32 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221232 134720464 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 479.66 Current children cumulated vsize (Kb) 11504 [startup+490.033 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2263 0 3 0 48933 32 0 0 25 0 1 0 1844048995 9601024 2156 4294967295 134512640 135167914 3221224448 3221221408 134522497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2156 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 489.66 Current children cumulated vsize (Kb) 11504 [startup+500.034 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 49933 33 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221219536 134629069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 499.67 Current children cumulated vsize (Kb) 11504 [startup+510.034 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 50932 33 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221218948 134522496 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 509.66 Current children cumulated vsize (Kb) 11504 [startup+520.035 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 51933 33 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221220496 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 519.67 Current children cumulated vsize (Kb) 11504 [startup+530.036 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 52932 34 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221220016 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 529.67 Current children cumulated vsize (Kb) 11504 [startup+540.036 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 53932 34 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221220120 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 539.67 Current children cumulated vsize (Kb) 11504 [startup+550.037 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 54932 34 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221220256 134629402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 549.67 Current children cumulated vsize (Kb) 11504 [startup+560.038 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 55932 35 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221219792 134844689 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 559.68 Current children cumulated vsize (Kb) 11504 [startup+570.038 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 56932 35 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221221200 134696781 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 569.68 Current children cumulated vsize (Kb) 11504 [startup+580.039 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 57931 35 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221220080 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 579.67 Current children cumulated vsize (Kb) 11504 [startup+590.039 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 58931 35 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221220928 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 589.67 Current children cumulated vsize (Kb) 11504 [startup+600.04 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 59931 35 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221221088 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 599.67 Current children cumulated vsize (Kb) 11504 [startup+610.042 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2267 0 3 0 60931 36 0 0 25 0 1 0 1844048995 9601024 2160 4294967295 134512640 135167914 3221224448 3221219676 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2344 2160 162 162 0 2182 0 [pid=16081] vsize: 9376 Current children cumulated CPU time (s) 609.68 Current children cumulated vsize (Kb) 11504 [startup+620.042 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 61931 36 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221218460 134722660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 619.68 Current children cumulated vsize (Kb) 11860 [startup+630.043 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 62931 36 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221219536 134630818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 629.68 Current children cumulated vsize (Kb) 11860 [startup+640.043 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 63930 37 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221219792 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 639.68 Current children cumulated vsize (Kb) 11860 [startup+650.044 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 64930 37 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220048 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 649.68 Current children cumulated vsize (Kb) 11860 [startup+660.044 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 65930 37 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220496 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 659.68 Current children cumulated vsize (Kb) 11860 [startup+670.046 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 66930 37 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220656 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 669.68 Current children cumulated vsize (Kb) 11860 [startup+680.046 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 67929 38 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220572 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 679.68 Current children cumulated vsize (Kb) 11860 [startup+690.046 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 68929 38 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221221904 134844691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 689.68 Current children cumulated vsize (Kb) 11860 [startup+700.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 69930 38 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220480 134845890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 699.69 Current children cumulated vsize (Kb) 11860 [startup+710.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 70929 39 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220704 134722539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 709.69 Current children cumulated vsize (Kb) 11860 [startup+720.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 71929 39 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220232 134522701 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 719.69 Current children cumulated vsize (Kb) 11860 [startup+730.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 72929 39 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221220832 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 729.69 Current children cumulated vsize (Kb) 11860 [startup+740.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2366 0 3 0 73929 40 0 0 25 0 1 0 1844048995 9965568 2217 4294967295 134512640 135167914 3221224448 3221221760 134693582 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2433 2217 162 162 0 2271 0 [pid=16081] vsize: 9732 Current children cumulated CPU time (s) 739.7 Current children cumulated vsize (Kb) 11860 [startup+750.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2398 0 3 0 74929 40 0 0 25 0 1 0 1844048995 10006528 2249 4294967295 134512640 135167914 3221224448 3221220176 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2443 2249 162 162 0 2281 0 [pid=16081] vsize: 9772 Current children cumulated CPU time (s) 749.7 Current children cumulated vsize (Kb) 11900 [startup+760.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2398 0 3 0 75928 40 0 0 25 0 1 0 1844048995 10006528 2249 4294967295 134512640 135167914 3221224448 3221221792 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2443 2249 162 162 0 2281 0 [pid=16081] vsize: 9772 Current children cumulated CPU time (s) 759.69 Current children cumulated vsize (Kb) 11900 [startup+770.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 76926 42 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221217552 134722532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 769.69 Current children cumulated vsize (Kb) 13352 [startup+780.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 77926 43 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221218256 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 779.7 Current children cumulated vsize (Kb) 13352 [startup+790.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 78926 43 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221218400 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 789.7 Current children cumulated vsize (Kb) 13352 [startup+800.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 79925 43 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219356 134522320 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 799.69 Current children cumulated vsize (Kb) 13352 [startup+810.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 80925 44 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219456 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 809.7 Current children cumulated vsize (Kb) 13352 [startup+820.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 81925 44 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219292 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 819.7 Current children cumulated vsize (Kb) 13352 [startup+830.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 82924 44 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219124 134844636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 829.69 Current children cumulated vsize (Kb) 13352 [startup+840.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 83925 44 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219616 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 839.7 Current children cumulated vsize (Kb) 13352 [startup+850.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 84924 44 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219856 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 849.69 Current children cumulated vsize (Kb) 13352 [startup+860.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 85924 45 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220576 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 859.7 Current children cumulated vsize (Kb) 13352 [startup+870.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 86924 45 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219328 134843015 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 869.7 Current children cumulated vsize (Kb) 13352 [startup+880.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 87924 45 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220400 134694329 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 879.7 Current children cumulated vsize (Kb) 13352 [startup+890.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 88924 46 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219552 134844647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 889.71 Current children cumulated vsize (Kb) 13352 [startup+900.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 89924 46 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220304 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 899.71 Current children cumulated vsize (Kb) 13352 [startup+910.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 90924 46 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220408 134849087 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 909.71 Current children cumulated vsize (Kb) 13352 [startup+920.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 91924 46 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220000 134693582 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 919.71 Current children cumulated vsize (Kb) 13352 [startup+930.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 92924 46 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220588 134694368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 929.71 Current children cumulated vsize (Kb) 13352 [startup+940.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 93924 46 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221632 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 939.71 Current children cumulated vsize (Kb) 13352 [startup+950.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 94923 46 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220208 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 949.7 Current children cumulated vsize (Kb) 13352 [startup+960.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 95923 47 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220124 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 959.71 Current children cumulated vsize (Kb) 13352 [startup+970.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 96923 47 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220880 134844672 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 969.71 Current children cumulated vsize (Kb) 13352 [startup+980.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 97923 47 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220188 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 979.71 Current children cumulated vsize (Kb) 13352 [startup+990.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 98922 48 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220924 134849088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 989.71 Current children cumulated vsize (Kb) 13352 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 99921 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220860 134723267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 999.71 Current children cumulated vsize (Kb) 13352 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 100921 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219884 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1009.71 Current children cumulated vsize (Kb) 13352 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 101922 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220208 134694495 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1019.72 Current children cumulated vsize (Kb) 13352 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 102922 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221264 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1029.72 Current children cumulated vsize (Kb) 13352 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 103922 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221280 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1039.72 Current children cumulated vsize (Kb) 13352 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 104922 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220560 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1049.72 Current children cumulated vsize (Kb) 13352 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 105922 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221228 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1059.72 Current children cumulated vsize (Kb) 13352 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 106922 49 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221600 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1069.72 Current children cumulated vsize (Kb) 13352 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 107922 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221219968 134845921 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1079.73 Current children cumulated vsize (Kb) 13352 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 108923 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220912 134522828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1089.74 Current children cumulated vsize (Kb) 13352 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 109923 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221636 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1099.74 Current children cumulated vsize (Kb) 13352 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 110923 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221228 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1109.74 Current children cumulated vsize (Kb) 13352 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 111923 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221220656 134845913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1119.74 Current children cumulated vsize (Kb) 13352 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 112923 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221456 134849122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1129.74 Current children cumulated vsize (Kb) 13352 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 113923 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221920 134696236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1139.74 Current children cumulated vsize (Kb) 13352 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 114924 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221222080 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1149.75 Current children cumulated vsize (Kb) 13352 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 115924 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221296 134629153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1159.75 Current children cumulated vsize (Kb) 13352 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 116924 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221221992 134849057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1169.75 Current children cumulated vsize (Kb) 13352 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2843 0 3 0 117924 50 0 0 25 0 1 0 1844048995 11493376 2569 4294967295 134512640 135167914 3221224448 3221222160 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2806 2569 162 162 0 2644 0 [pid=16081] vsize: 11224 Current children cumulated CPU time (s) 1179.75 Current children cumulated vsize (Kb) 13352 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2888 0 3 0 118924 50 0 0 25 0 1 0 1844048995 11173888 2514 4294967295 134512640 135167914 3221224448 3221218736 134844731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2728 2514 162 162 0 2566 0 [pid=16081] vsize: 10912 Current children cumulated CPU time (s) 1189.75 Current children cumulated vsize (Kb) 13040 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2914 0 3 0 119924 51 0 0 25 0 1 0 1844048995 11149312 2508 4294967295 134512640 135167914 3221224448 3221218832 134630738 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2722 2508 162 162 0 2560 0 [pid=16081] vsize: 10888 Current children cumulated CPU time (s) 1199.76 Current children cumulated vsize (Kb) 13016 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2914 0 3 0 120924 51 0 0 25 0 1 0 1844048995 11149312 2508 4294967295 134512640 135167914 3221224448 3221220560 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2722 2508 162 162 0 2560 0 [pid=16081] vsize: 10888 Current children cumulated CPU time (s) 1209.76 Current children cumulated vsize (Kb) 13016 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16081 Raw data (/proc/16076/stat): 16076 (minisat+_script) S 16075 16076 4419 0 -1 0 314 362 0 0 0 0 1 0 21 0 1 0 1844048988 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16076/statm): 532 234 485 147 0 385 0 [pid=16076] vsize: 2128 Raw data (/proc/16081/stat): 16081 (minisat+_bignum) R 16076 16076 4419 0 -1 0 2914 0 3 0 120924 51 0 0 25 0 1 0 1844048995 11149312 2508 4294967295 134512640 135167914 3221224448 3221220536 134845939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16081/statm): 2722 2508 162 162 0 2560 0 [pid=16081] vsize: 10888 Current children cumulated CPU time (s) 1209.76 Current children cumulated vsize (Kb) 13016 Sending SIGTERM to -16076 Sleeping 2 seconds One traced child (pid=16076) ended because it received signal 15 (SIGTERM) One traced child (pid=16081) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.09 CPU time (s): 1209.77 CPU user time (s): 1209.25 CPU system time (s): 0.516921 CPU usage (%): 99.9735 Max. virtual memory (cumulated for all children) (Kb): 13352
ERROR: no interpretation found !