Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-modglob.opb |
MD5SUM | 2de26b7af333f64c2208bd35d6d5a979 |
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 | 9818 |
Biggest coefficient in the objective function | 22009559908352000000 |
Number of bits for the biggest coefficient in the objective function | 65 |
Sum of the numbers in the objective function | 1485172925553747165184 |
Number of bits of the sum of numbers in the objective function | 71 |
Biggest number in a constraint | 22009559908352000000 |
Number of bits of the biggest number in a constraint | 65 |
Biggest sum of numbers in a constraint | 1485172925553747165184 |
Number of bits of the biggest sum of numbers | 71 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 9818 |
Total number of constraints | 389 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 98 |
Number of constraints which are nor clauses,nor cardinality constraints | 291 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 270 |
LAUNCH ON wulflinc5 THE 2005-09-19 03:18:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2871 boxname=wulflinc5 idbench=527 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2de26b7af333f64c2208bd35d6d5a979 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-modglob.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-modglob.opb IDLAUNCH: 2871 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 904192 kB Buffers: 35248 kB Cached: 71140 kB SwapCached: 780 kB Active: 73904 kB Inactive: 35256 kB HighTotal: 131008 kB HighFree: 56196 kB LowTotal: 903652 kB LowFree: 847996 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 64 kB Writeback: 0 kB Mapped: 5804 kB Slab: 15736 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:38:20 (client local time) WITH STATUS 0 IN 1202.99 SECONDS stats: 2871 7 1202.99 0
c Parsing PB file... c PARSE ERROR! [line 426] 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/16466/stat): 16466 (minisat+_script) R 16465 16466 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788372785 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/16466/statm): 174 3 169 147 0 27 0 [pid=16466] 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=16467 New process pid=16468 New process pid=16469 execve syscall for /bin/sed executable One traced child (pid=16468) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=16469) exited with status: 0 One traced child (pid=16467) exited with status: 0 New process pid=16470 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-modglob.opb One traced child (pid=16470) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=16471 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-modglob.opb [startup+10.0031 s] Raw data (loadavg): 0.94 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 5232 0 0 0 945 22 0 0 25 0 1 0 1788372792 19324928 4540 4294967295 134512640 135167914 3221224448 3221198804 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 4718 4540 162 162 0 4556 0 [pid=16471] vsize: 18872 Current children cumulated CPU time (s) 9.68 Current children cumulated vsize (Kb) 21000 [startup+20.0049 s] Raw data (loadavg): 0.95 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 10872 0 0 0 1897 44 0 0 25 0 1 0 1788372792 39727104 9521 4294967295 134512640 135167914 3221224448 3221198736 134624994 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 9699 9521 162 162 0 9537 0 [pid=16471] vsize: 38796 Current children cumulated CPU time (s) 19.42 Current children cumulated vsize (Kb) 40924 [startup+30.0056 s] Raw data (loadavg): 0.96 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 17548 0 0 0 2844 70 0 0 25 0 1 0 1788372792 61673472 14879 4294967295 134512640 135167914 3221224448 3221196384 134847159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 15057 14879 162 162 0 14895 0 [pid=16471] vsize: 60228 Current children cumulated CPU time (s) 29.15 Current children cumulated vsize (Kb) 62356 [startup+40.0064 s] Raw data (loadavg): 0.97 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 22006 0 0 0 3799 90 0 0 25 0 1 0 1788372792 79933440 19337 4294967295 134512640 135167914 3221224448 3221197468 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 19515 19337 162 162 0 19353 0 [pid=16471] vsize: 78060 Current children cumulated CPU time (s) 38.9 Current children cumulated vsize (Kb) 80188 [startup+50.0071 s] Raw data (loadavg): 0.97 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 30778 0 0 0 4748 117 0 0 25 0 1 0 1788372792 105062400 25472 4294967295 134512640 135167914 3221224448 3221197212 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/16471/statm): 25650 25472 162 162 0 25488 0 [pid=16471] vsize: 102600 Current children cumulated CPU time (s) 48.66 Current children cumulated vsize (Kb) 104728 [startup+60.0068 s] Raw data (loadavg): 0.97 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 35207 0 0 0 5699 138 0 0 25 0 1 0 1788372792 123203584 29901 4294967295 134512640 135167914 3221224448 3221197708 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/16471/statm): 30079 29901 162 162 0 29917 0 [pid=16471] vsize: 120316 Current children cumulated CPU time (s) 58.38 Current children cumulated vsize (Kb) 122444 [startup+70.0076 s] Raw data (loadavg): 0.98 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 39550 0 0 0 6650 156 0 0 22 0 1 0 1788372792 140992512 34244 4294967295 134512640 135167914 3221224448 3221195908 134849086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 34422 34244 162 162 0 34260 0 [pid=16471] vsize: 137688 Current children cumulated CPU time (s) 68.07 Current children cumulated vsize (Kb) 139816 [startup+80.0083 s] Raw data (loadavg): 0.98 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 54026 0 0 0 7582 197 0 0 25 0 1 0 1788372792 200286208 48720 4294967295 134512640 135167914 3221224448 3221198128 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 48898 48720 162 162 0 48736 0 [pid=16471] vsize: 195592 Current children cumulated CPU time (s) 77.8 Current children cumulated vsize (Kb) 197720 [startup+90.0091 s] Raw data (loadavg): 0.98 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 56879 0 0 0 8549 212 0 0 25 0 1 0 1788372792 190373888 46300 4294967295 134512640 135167914 3221224448 3221195740 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/16471/statm): 46478 46300 162 162 0 46316 0 [pid=16471] vsize: 185912 Current children cumulated CPU time (s) 87.62 Current children cumulated vsize (Kb) 188040 [startup+100.01 s] Raw data (loadavg): 0.98 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 61184 0 0 0 9504 232 0 0 25 0 1 0 1788372792 208007168 50605 4294967295 134512640 135167914 3221224448 3221201024 134695563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 50783 50605 162 162 0 50621 0 [pid=16471] vsize: 203132 Current children cumulated CPU time (s) 97.37 Current children cumulated vsize (Kb) 205260 [startup+110.011 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 65476 0 0 0 10453 252 0 0 25 0 1 0 1788372792 225587200 54897 4294967295 134512640 135167914 3221224448 3221196192 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 55075 54897 162 162 0 54913 0 [pid=16471] vsize: 220300 Current children cumulated CPU time (s) 107.06 Current children cumulated vsize (Kb) 222428 [startup+120.012 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 69752 0 0 0 11405 271 0 0 25 0 1 0 1788372792 243101696 59173 4294967295 134512640 135167914 3221224448 3221196316 134845882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 59351 59173 162 162 0 59189 0 [pid=16471] vsize: 237404 Current children cumulated CPU time (s) 116.77 Current children cumulated vsize (Kb) 239532 [startup+130.013 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 73905 0 0 0 12363 289 0 0 25 0 1 0 1788372792 260112384 63326 4294967295 134512640 135167914 3221224448 3221196088 134697257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 63504 63326 162 162 0 63342 0 [pid=16471] vsize: 254016 Current children cumulated CPU time (s) 126.53 Current children cumulated vsize (Kb) 256144 [startup+140.014 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 78024 0 0 0 13321 308 0 0 25 0 1 0 1788372792 276983808 67445 4294967295 134512640 135167914 3221224448 3221197876 134697380 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 67623 67445 162 162 0 67461 0 [pid=16471] vsize: 270492 Current children cumulated CPU time (s) 136.3 Current children cumulated vsize (Kb) 272620 [startup+150.015 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 82099 0 0 0 14277 327 0 0 25 0 1 0 1788372792 293675008 71520 4294967295 134512640 135167914 3221224448 3221196800 134694517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 71698 71520 162 162 0 71536 0 [pid=16471] vsize: 286792 Current children cumulated CPU time (s) 146.05 Current children cumulated vsize (Kb) 288920 [startup+160.014 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 106930 0 0 0 15195 386 0 0 25 0 1 0 1788372792 395382784 96351 4294967295 134512640 135167914 3221224448 3221199916 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 96529 96351 162 162 0 96367 0 [pid=16471] vsize: 386116 Current children cumulated CPU time (s) 155.82 Current children cumulated vsize (Kb) 388244 [startup+170.015 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 107765 0 0 0 16185 391 0 0 25 0 1 0 1788372792 355606528 86640 4294967295 134512640 135167914 3221224448 3221197276 134695741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 86818 86640 162 162 0 86656 0 [pid=16471] vsize: 347272 Current children cumulated CPU time (s) 165.77 Current children cumulated vsize (Kb) 349400 [startup+180.015 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 111798 0 0 0 17143 408 0 0 25 0 1 0 1788372792 372125696 90673 4294967295 134512640 135167914 3221224448 3221195740 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/16471/statm): 90851 90673 162 162 0 90689 0 [pid=16471] vsize: 363404 Current children cumulated CPU time (s) 175.52 Current children cumulated vsize (Kb) 365532 [startup+190.017 s] Raw data (loadavg): 0.99 1.00 0.98 1/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 115757 0 0 0 18100 425 0 0 25 0 1 0 1788372792 388341760 94632 4294967295 134512640 135167914 3221224448 3221197436 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/16471/statm): 94810 94632 162 162 0 94648 0 [pid=16471] vsize: 379240 Current children cumulated CPU time (s) 185.26 Current children cumulated vsize (Kb) 381368 [startup+200.017 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 119696 0 0 0 19056 443 0 0 25 0 1 0 1788372792 404475904 98571 4294967295 134512640 135167914 3221224448 3221207788 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 98749 98571 162 162 0 98587 0 [pid=16471] vsize: 394996 Current children cumulated CPU time (s) 195 Current children cumulated vsize (Kb) 397124 [startup+210.017 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 123633 0 0 0 20015 460 0 0 25 0 1 0 1788372792 420601856 102508 4294967295 134512640 135167914 3221224448 3221198080 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 102686 102508 162 162 0 102524 0 [pid=16471] vsize: 410744 Current children cumulated CPU time (s) 204.76 Current children cumulated vsize (Kb) 412872 [startup+220.019 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 127570 0 0 0 20973 477 0 0 25 0 1 0 1788372792 436727808 106445 4294967295 134512640 135167914 3221224448 3221196264 134846853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 106623 106445 162 162 0 106461 0 [pid=16471] vsize: 426492 Current children cumulated CPU time (s) 214.51 Current children cumulated vsize (Kb) 428620 [startup+230.02 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 131454 0 0 0 21932 494 0 0 25 0 1 0 1788372792 452636672 110329 4294967295 134512640 135167914 3221224448 3221196480 134843160 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 110507 110329 162 162 0 110345 0 [pid=16471] vsize: 442028 Current children cumulated CPU time (s) 224.27 Current children cumulated vsize (Kb) 444156 [startup+240.019 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 135317 0 0 0 22890 510 0 0 25 0 1 0 1788372792 468459520 114192 4294967295 134512640 135167914 3221224448 3221199932 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 114370 114192 162 162 0 114208 0 [pid=16471] vsize: 457480 Current children cumulated CPU time (s) 234.01 Current children cumulated vsize (Kb) 459608 [startup+250.02 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 139118 0 0 0 23846 527 0 0 25 0 1 0 1788372792 484028416 117993 4294967295 134512640 135167914 3221224448 3221195648 134696103 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 118171 117993 162 162 0 118009 0 [pid=16471] vsize: 472684 Current children cumulated CPU time (s) 243.74 Current children cumulated vsize (Kb) 474812 [startup+260.021 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 142883 0 0 0 24804 545 0 0 25 0 1 0 1788372792 499449856 121758 4294967295 134512640 135167914 3221224448 3221198064 134849066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 121936 121758 162 162 0 121774 0 [pid=16471] vsize: 487744 Current children cumulated CPU time (s) 253.5 Current children cumulated vsize (Kb) 489872 [startup+270.021 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 146549 0 0 0 25767 560 0 0 25 0 1 0 1788372792 514465792 125424 4294967295 134512640 135167914 3221224448 3221197152 134843406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 125602 125424 162 162 0 125440 0 [pid=16471] vsize: 502408 Current children cumulated CPU time (s) 263.28 Current children cumulated vsize (Kb) 504536 [startup+280.022 s] Raw data (loadavg): 0.99 1.00 0.98 1/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 150192 0 0 0 26728 577 0 0 25 0 1 0 1788372792 529387520 129067 4294967295 134512640 135167914 3221224448 3221196364 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/16471/statm): 129245 129067 162 162 0 129083 0 [pid=16471] vsize: 516980 Current children cumulated CPU time (s) 273.06 Current children cumulated vsize (Kb) 519108 [startup+290.022 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 153868 0 0 0 27686 595 0 0 25 0 1 0 1788372792 544444416 132743 4294967295 134512640 135167914 3221224448 3221196288 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 132921 132743 162 162 0 132759 0 [pid=16471] vsize: 531684 Current children cumulated CPU time (s) 282.82 Current children cumulated vsize (Kb) 533812 [startup+300.023 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157525 0 0 0 28649 608 0 0 25 0 1 0 1788372792 559435776 136400 4294967295 134512640 135167914 3221224448 3221195744 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16471/statm): 136581 136400 162 162 0 136419 0 [pid=16471] vsize: 546324 Current children cumulated CPU time (s) 292.58 Current children cumulated vsize (Kb) 548452 [startup+310.023 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157884 0 0 0 29642 613 0 0 25 0 1 0 1788372792 474517504 115668 4294967295 134512640 135167914 3221224448 3221223236 134623425 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115668 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 302.56 Current children cumulated vsize (Kb) 465524 [startup+320.024 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 30642 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217056 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 312.56 Current children cumulated vsize (Kb) 465524 [startup+330.025 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 31642 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217596 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 322.56 Current children cumulated vsize (Kb) 465524 [startup+340.025 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 32643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217768 134693553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 332.57 Current children cumulated vsize (Kb) 465524 [startup+350.025 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 33643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218128 134629138 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 342.57 Current children cumulated vsize (Kb) 465524 [startup+360.026 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 34643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217488 134845909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 352.57 Current children cumulated vsize (Kb) 465524 [startup+370.027 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 35643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217592 134694321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 362.57 Current children cumulated vsize (Kb) 465524 [startup+380.028 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 36644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218620 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 372.58 Current children cumulated vsize (Kb) 465524 [startup+390.028 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 37644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217756 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 382.58 Current children cumulated vsize (Kb) 465524 [startup+400.029 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 38644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218112 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 392.58 Current children cumulated vsize (Kb) 465524 [startup+410.03 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 39644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218944 134522502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 402.58 Current children cumulated vsize (Kb) 465524 [startup+420.031 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 40645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218936 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 412.59 Current children cumulated vsize (Kb) 465524 [startup+430.031 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 41645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219264 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 422.59 Current children cumulated vsize (Kb) 465524 [startup+440.032 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 42645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218496 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 432.59 Current children cumulated vsize (Kb) 465524 [startup+450.033 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 43645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217856 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 442.59 Current children cumulated vsize (Kb) 465524 [startup+460.034 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 44646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218736 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 452.6 Current children cumulated vsize (Kb) 465524 [startup+470.034 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 45646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219328 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 462.6 Current children cumulated vsize (Kb) 465524 [startup+480.035 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 46646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218624 134843404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 472.6 Current children cumulated vsize (Kb) 465524 [startup+490.036 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 47646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219352 134842997 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 482.6 Current children cumulated vsize (Kb) 465524 [startup+500.037 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 48647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218048 134723225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 492.61 Current children cumulated vsize (Kb) 465524 [startup+510.037 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 49647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218816 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 502.61 Current children cumulated vsize (Kb) 465524 [startup+520.038 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 50647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218912 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 512.61 Current children cumulated vsize (Kb) 465524 [startup+530.039 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 51647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218080 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 522.61 Current children cumulated vsize (Kb) 465524 [startup+540.039 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 52647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219532 134693552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 532.61 Current children cumulated vsize (Kb) 465524 [startup+550.039 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 53648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218588 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 542.62 Current children cumulated vsize (Kb) 465524 [startup+560.04 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 54648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 552.62 Current children cumulated vsize (Kb) 465524 [startup+570.041 s] Raw data (loadavg): 0.99 1.00 0.98 3/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 55648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219504 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 562.62 Current children cumulated vsize (Kb) 465524 [startup+580.042 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 56648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218412 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 572.62 Current children cumulated vsize (Kb) 465524 [startup+590.042 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 57649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218288 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 582.63 Current children cumulated vsize (Kb) 465524 [startup+600.043 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 58649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219684 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 592.63 Current children cumulated vsize (Kb) 465524 [startup+610.044 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 59649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218476 134522184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 602.63 Current children cumulated vsize (Kb) 465524 [startup+620.045 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 60649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218992 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 612.63 Current children cumulated vsize (Kb) 465524 [startup+630.045 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 61650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218272 134694545 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 622.64 Current children cumulated vsize (Kb) 465524 [startup+640.045 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 62650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219888 134629080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 632.64 Current children cumulated vsize (Kb) 465524 [startup+650.046 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 63650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217760 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 642.64 Current children cumulated vsize (Kb) 465524 [startup+660.047 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 64650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218256 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 652.64 Current children cumulated vsize (Kb) 465524 [startup+670.048 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 65651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218032 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 662.65 Current children cumulated vsize (Kb) 465524 [startup+680.049 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 66651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220192 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 672.65 Current children cumulated vsize (Kb) 465524 [startup+690.05 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 67651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218208 134696745 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 682.65 Current children cumulated vsize (Kb) 465524 [startup+700.051 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 68651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219104 134723225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 692.65 Current children cumulated vsize (Kb) 465524 [startup+710.051 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 69652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218648 134694321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 702.66 Current children cumulated vsize (Kb) 465524 [startup+720.052 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 70652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219856 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 712.66 Current children cumulated vsize (Kb) 465524 [startup+730.053 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 71652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 722.66 Current children cumulated vsize (Kb) 465524 [startup+740.053 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 72652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218368 134845890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 732.66 Current children cumulated vsize (Kb) 465524 [startup+750.053 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 73653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218368 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 742.67 Current children cumulated vsize (Kb) 465524 [startup+760.054 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 74653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219856 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 752.67 Current children cumulated vsize (Kb) 465524 [startup+770.055 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 75653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134696745 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 762.67 Current children cumulated vsize (Kb) 465524 [startup+780.056 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 76653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218640 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 772.67 Current children cumulated vsize (Kb) 465524 [startup+790.055 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 77653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219296 134720472 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 782.67 Current children cumulated vsize (Kb) 465524 [startup+800.056 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 78654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219644 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 792.68 Current children cumulated vsize (Kb) 465524 [startup+810.057 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 79654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218480 134629167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 802.68 Current children cumulated vsize (Kb) 465524 [startup+820.057 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 80654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218472 134693744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 812.68 Current children cumulated vsize (Kb) 465524 [startup+830.058 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 81654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218624 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 822.68 Current children cumulated vsize (Kb) 465524 [startup+840.058 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 82655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219184 134630940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 832.69 Current children cumulated vsize (Kb) 465524 [startup+850.059 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 83655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219100 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 842.69 Current children cumulated vsize (Kb) 465524 [startup+860.059 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 84655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220048 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 852.69 Current children cumulated vsize (Kb) 465524 [startup+870.061 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 85655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218824 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 862.69 Current children cumulated vsize (Kb) 465524 [startup+880.062 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 86656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219088 134843026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 872.7 Current children cumulated vsize (Kb) 465524 [startup+890.062 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 87656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218192 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 882.7 Current children cumulated vsize (Kb) 465524 [startup+900.062 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 88656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218468 134843031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 892.7 Current children cumulated vsize (Kb) 465524 [startup+910.063 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 89656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219868 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 902.7 Current children cumulated vsize (Kb) 465524 [startup+920.064 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 90657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219000 134693808 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 912.71 Current children cumulated vsize (Kb) 465524 [startup+930.065 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 91657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219328 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 922.71 Current children cumulated vsize (Kb) 465524 [startup+940.065 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 92657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218080 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 932.71 Current children cumulated vsize (Kb) 465524 [startup+950.066 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 93657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219280 134843153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 942.71 Current children cumulated vsize (Kb) 465524 [startup+960.067 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 94658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220576 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 952.72 Current children cumulated vsize (Kb) 465524 [startup+970.069 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 95658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219472 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 962.72 Current children cumulated vsize (Kb) 465524 [startup+980.069 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 96658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219352 134696177 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 972.72 Current children cumulated vsize (Kb) 465524 [startup+990.069 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 97658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219124 134845880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 982.72 Current children cumulated vsize (Kb) 465524 [startup+1000.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 98659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219440 134844682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 992.73 Current children cumulated vsize (Kb) 465524 [startup+1010.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 99659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220144 134844731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1002.73 Current children cumulated vsize (Kb) 465524 [startup+1020.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 100659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219008 134629216 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1012.73 Current children cumulated vsize (Kb) 465524 [startup+1030.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 101659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217948 134693728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1022.73 Current children cumulated vsize (Kb) 465524 [startup+1040.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 102659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218440 134845939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1032.73 Current children cumulated vsize (Kb) 465524 [startup+1050.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 103660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217884 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1042.74 Current children cumulated vsize (Kb) 465524 [startup+1060.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 104660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219520 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1052.74 Current children cumulated vsize (Kb) 465524 [startup+1070.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 105660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218956 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1062.74 Current children cumulated vsize (Kb) 465524 [startup+1080.07 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 106660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218720 134718181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1072.74 Current children cumulated vsize (Kb) 465524 [startup+1090.08 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 107661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218284 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1082.75 Current children cumulated vsize (Kb) 465524 [startup+1100.08 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 108661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218384 134696342 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1092.75 Current children cumulated vsize (Kb) 465524 [startup+1110.08 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 109661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218832 134629290 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1102.75 Current children cumulated vsize (Kb) 465524 [startup+1120.08 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 110661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217880 134723290 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1112.75 Current children cumulated vsize (Kb) 465524 [startup+1130.08 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 111662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219884 134694480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1122.76 Current children cumulated vsize (Kb) 465524 [startup+1140.08 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 112662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219168 134693561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1132.76 Current children cumulated vsize (Kb) 465524 [startup+1150.08 s] Raw data (loadavg): 0.99 1.00 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 113662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218208 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1142.76 Current children cumulated vsize (Kb) 465524 [startup+1160.08 s] Raw data (loadavg): 1.07 1.02 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 114662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218720 134844637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1152.76 Current children cumulated vsize (Kb) 465524 [startup+1170.08 s] Raw data (loadavg): 1.06 1.02 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 115663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219616 134844708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1162.77 Current children cumulated vsize (Kb) 465524 [startup+1180.08 s] Raw data (loadavg): 1.05 1.01 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 116663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220144 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1172.77 Current children cumulated vsize (Kb) 465524 [startup+1190.08 s] Raw data (loadavg): 1.04 1.01 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 117663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134843153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1182.77 Current children cumulated vsize (Kb) 465524 [startup+1200.08 s] Raw data (loadavg): 1.03 1.01 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 118663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218496 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1192.77 Current children cumulated vsize (Kb) 465524 [startup+1210.08 s] Raw data (loadavg): 1.03 1.01 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 119664 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219016 134629347 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1202.78 Current children cumulated vsize (Kb) 465524 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.03 1.01 0.98 2/57 16471 Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16466/statm): 532 234 485 147 0 385 0 [pid=16466] vsize: 2128 Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 119664 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218816 134522206 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0 [pid=16471] vsize: 463396 Current children cumulated CPU time (s) 1202.78 Current children cumulated vsize (Kb) 465524 Sending SIGTERM to -16466 Sleeping 2 seconds One traced child (pid=16466) ended because it received signal 15 (SIGTERM) One traced child (pid=16471) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.3 CPU time (s): 1202.99 CPU user time (s): 1196.64 CPU system time (s): 6.35203 CPU usage (%): 99.3961 Max. virtual memory (cumulated for all children) (Kb): 548452
ERROR: no interpretation found !