Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-stair.opb |
MD5SUM | f2a6dc8d2697a7f5959c84e4079088c9 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 30 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 1073741823 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 528959045369856 |
Number of bits of the biggest number in a constraint | 49 |
Biggest sum of numbers in a constraint | 3702118998041541 |
Number of bits of the biggest sum of numbers | 52 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 204.283 |
Number of variables | 11454 |
Total number of constraints | 362 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 362 |
Minimum length of a constraint | 13 |
Maximum length of a constraint | 810 |
LAUNCH ON wulflinc5 THE 2005-09-18 20:37:56 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2823 boxname=wulflinc5 idbench=479 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f2a6dc8d2697a7f5959c84e4079088c9 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-stair.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-stair.opb IDLAUNCH: 2823 /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: 912432 kB Buffers: 34424 kB Cached: 63804 kB SwapCached: 780 kB Active: 65052 kB Inactive: 35892 kB HighTotal: 131008 kB HighFree: 63532 kB LowTotal: 903652 kB LowFree: 848900 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5804 kB Slab: 15652 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 20:58:06 (client local time) WITH STATUS 0 IN 1209.91 SECONDS stats: 2823 7 1209.91 0
c Parsing PB file... c PARSE ERROR! [line 478] 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/13392/stat): 13392 (minisat+_script) R 13391 13392 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785971103 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/13392/statm): 174 3 169 147 0 27 0 [pid=13392] 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=13393 New process pid=13394 New process pid=13395 execve syscall for /bin/sed executable One traced child (pid=13394) 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=13395) exited with status: 0 One traced child (pid=13393) exited with status: 0 New process pid=13396 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-stair.opb One traced child (pid=13396) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=13397 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-stair.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 945 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221218292 134522324 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 9.61 Current children cumulated vsize (Kb) 12156 [startup+20.0043 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 1946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219340 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 19.62 Current children cumulated vsize (Kb) 12156 [startup+30.005 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 2946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219100 134723267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 29.62 Current children cumulated vsize (Kb) 12156 [startup+40.0058 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 3946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219440 134845895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 39.62 Current children cumulated vsize (Kb) 12156 [startup+50.0065 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 4946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219216 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 49.62 Current children cumulated vsize (Kb) 12156 [startup+60.0062 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 5946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219376 134628744 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 59.62 Current children cumulated vsize (Kb) 12156 [startup+70.007 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 6946 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220056 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 69.63 Current children cumulated vsize (Kb) 12156 [startup+80.0077 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 7947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219552 134629445 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 79.64 Current children cumulated vsize (Kb) 12156 [startup+90.0085 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 8947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220048 134693582 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 89.64 Current children cumulated vsize (Kb) 12156 [startup+100.009 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 9947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219680 134694517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 99.64 Current children cumulated vsize (Kb) 12156 [startup+110.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 10947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220056 134693808 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 109.64 Current children cumulated vsize (Kb) 12156 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 11947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220044 134722660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 119.64 Current children cumulated vsize (Kb) 12156 [startup+130.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 12948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220308 134844636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 129.65 Current children cumulated vsize (Kb) 12156 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 13948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220524 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 139.65 Current children cumulated vsize (Kb) 12156 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 14948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220904 134722513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 149.65 Current children cumulated vsize (Kb) 12156 [startup+160.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 15948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220588 134694551 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 159.65 Current children cumulated vsize (Kb) 12156 [startup+170.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 16948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221376 134696366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 169.65 Current children cumulated vsize (Kb) 12156 [startup+180.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 17949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220672 134696726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 179.66 Current children cumulated vsize (Kb) 12156 [startup+190.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 18949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220832 134845930 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 189.66 Current children cumulated vsize (Kb) 12156 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 19949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221128 134629047 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 199.66 Current children cumulated vsize (Kb) 12156 [startup+210.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 20949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221392 134696578 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 209.66 Current children cumulated vsize (Kb) 12156 [startup+220.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 21949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220864 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 219.66 Current children cumulated vsize (Kb) 12156 [startup+230.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 22951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221264 134694435 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 229.68 Current children cumulated vsize (Kb) 12156 [startup+240.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 23951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221552 134843420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 239.68 Current children cumulated vsize (Kb) 12156 [startup+250.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 24951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221360 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 249.68 Current children cumulated vsize (Kb) 12156 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 25951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221216 134723225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 259.68 Current children cumulated vsize (Kb) 12156 [startup+270.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 26952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221424 134722521 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 269.69 Current children cumulated vsize (Kb) 12156 [startup+280.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 27952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221624 134722513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 279.69 Current children cumulated vsize (Kb) 12156 [startup+290.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 28952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221264 134849122 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 289.69 Current children cumulated vsize (Kb) 12156 [startup+300.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 29952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221552 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 299.69 Current children cumulated vsize (Kb) 12156 [startup+310.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 30952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221392 134696233 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0 [pid=13397] vsize: 10028 Current children cumulated CPU time (s) 309.69 Current children cumulated vsize (Kb) 12156 [startup+320.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 31951 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221218428 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 319.7 Current children cumulated vsize (Kb) 13220 [startup+330.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 32951 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221218764 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 329.7 Current children cumulated vsize (Kb) 13220 [startup+340.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 33951 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221219460 134843031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 339.7 Current children cumulated vsize (Kb) 13220 [startup+350.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 34952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221220016 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 349.71 Current children cumulated vsize (Kb) 13220 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 35952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221220320 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 359.71 Current children cumulated vsize (Kb) 13220 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 36952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221220736 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 369.71 Current children cumulated vsize (Kb) 13220 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 37952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221060 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 379.71 Current children cumulated vsize (Kb) 13220 [startup+390.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 38952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221184 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 389.71 Current children cumulated vsize (Kb) 13220 [startup+400.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 39953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221424 134522468 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 399.72 Current children cumulated vsize (Kb) 13220 [startup+410.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 40953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221280 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 409.72 Current children cumulated vsize (Kb) 13220 [startup+420.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 41953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221640 134693826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 419.72 Current children cumulated vsize (Kb) 13220 [startup+430.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 42953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221222256 134844708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 429.72 Current children cumulated vsize (Kb) 13220 [startup+440.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 43954 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221222256 134696738 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0 [pid=13397] vsize: 11092 Current children cumulated CPU time (s) 439.73 Current children cumulated vsize (Kb) 13220 [startup+450.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 44954 17 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221217148 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 449.73 Current children cumulated vsize (Kb) 13232 [startup+460.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 45954 17 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221217944 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 459.73 Current children cumulated vsize (Kb) 13232 [startup+470.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 46954 17 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218652 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 469.73 Current children cumulated vsize (Kb) 13232 [startup+480.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 47954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218192 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 479.74 Current children cumulated vsize (Kb) 13232 [startup+490.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 48954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218824 134522321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 489.74 Current children cumulated vsize (Kb) 13232 [startup+500.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 49954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218428 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 499.74 Current children cumulated vsize (Kb) 13232 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 50954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219248 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 509.74 Current children cumulated vsize (Kb) 13232 [startup+520.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 51954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219536 134630875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 519.75 Current children cumulated vsize (Kb) 13232 [startup+530.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 52954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219264 134844676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 529.75 Current children cumulated vsize (Kb) 13232 [startup+540.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 53954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220016 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 539.75 Current children cumulated vsize (Kb) 13232 [startup+550.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 54954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219296 134718188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 549.75 Current children cumulated vsize (Kb) 13232 [startup+560.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 55954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219492 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 559.75 Current children cumulated vsize (Kb) 13232 [startup+570.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 56954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220048 134693582 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 569.75 Current children cumulated vsize (Kb) 13232 [startup+580.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 57955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219768 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 579.76 Current children cumulated vsize (Kb) 13232 [startup+590.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 58955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219520 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 589.76 Current children cumulated vsize (Kb) 13232 [startup+600.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 59955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219804 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 599.76 Current children cumulated vsize (Kb) 13232 [startup+610.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 60955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220184 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 609.76 Current children cumulated vsize (Kb) 13232 [startup+620.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 61956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219836 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 619.77 Current children cumulated vsize (Kb) 13232 [startup+630.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 62956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 629.77 Current children cumulated vsize (Kb) 13232 [startup+640.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 63956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220400 134849096 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 639.77 Current children cumulated vsize (Kb) 13232 [startup+650.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 64956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220512 134723288 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 649.77 Current children cumulated vsize (Kb) 13232 [startup+660.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 65956 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220716 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 659.78 Current children cumulated vsize (Kb) 13232 [startup+670.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 66956 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220864 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 669.78 Current children cumulated vsize (Kb) 13232 [startup+680.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 67957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220576 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 679.79 Current children cumulated vsize (Kb) 13232 [startup+690.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 68957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221216 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 689.79 Current children cumulated vsize (Kb) 13232 [startup+700.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 69957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221200 134843036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 699.79 Current children cumulated vsize (Kb) 13232 [startup+710.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 70957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221024 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 709.79 Current children cumulated vsize (Kb) 13232 [startup+720.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 71957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220912 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 719.79 Current children cumulated vsize (Kb) 13232 [startup+730.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 72958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220848 134696285 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 729.8 Current children cumulated vsize (Kb) 13232 [startup+740.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 73958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221104 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 739.8 Current children cumulated vsize (Kb) 13232 [startup+750.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 74958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220912 134694528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 749.8 Current children cumulated vsize (Kb) 13232 [startup+760.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 75958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221008 134845933 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 759.8 Current children cumulated vsize (Kb) 13232 [startup+770.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 76958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221464 134696561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 769.8 Current children cumulated vsize (Kb) 13232 [startup+780.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 77959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221104 134849066 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 779.81 Current children cumulated vsize (Kb) 13232 [startup+790.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 78959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221248 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 789.81 Current children cumulated vsize (Kb) 13232 [startup+800.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 79959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220840 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 799.81 Current children cumulated vsize (Kb) 13232 [startup+810.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 80959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221488 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 809.81 Current children cumulated vsize (Kb) 13232 [startup+820.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 81959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 819.81 Current children cumulated vsize (Kb) 13232 [startup+830.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 82960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221760 134695257 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 829.82 Current children cumulated vsize (Kb) 13232 [startup+840.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 83960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221840 134628639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 839.82 Current children cumulated vsize (Kb) 13232 [startup+850.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 84960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221920 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 849.82 Current children cumulated vsize (Kb) 13232 [startup+860.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 85960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221564 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 859.82 Current children cumulated vsize (Kb) 13232 [startup+870.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 86961 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221222320 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0 [pid=13397] vsize: 11104 Current children cumulated CPU time (s) 869.83 Current children cumulated vsize (Kb) 13232 [startup+880.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 87960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217152 134845918 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 879.83 Current children cumulated vsize (Kb) 13796 [startup+890.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 88960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217584 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 889.83 Current children cumulated vsize (Kb) 13796 [startup+900.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 89960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217392 134849061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 899.83 Current children cumulated vsize (Kb) 13796 [startup+910.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 90960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217440 134844676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 909.83 Current children cumulated vsize (Kb) 13796 [startup+920.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 91961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217792 134844647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 919.84 Current children cumulated vsize (Kb) 13796 [startup+930.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 92961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218444 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 929.84 Current children cumulated vsize (Kb) 13796 [startup+940.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 93961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217856 134845903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 939.84 Current children cumulated vsize (Kb) 13796 [startup+950.079 s] Raw data (loadavg): 1.07 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 94961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218640 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 949.84 Current children cumulated vsize (Kb) 13796 [startup+960.08 s] Raw data (loadavg): 1.06 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 95962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218292 134522188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 959.85 Current children cumulated vsize (Kb) 13796 [startup+970.081 s] Raw data (loadavg): 1.05 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 96962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218652 134522320 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 969.85 Current children cumulated vsize (Kb) 13796 [startup+980.082 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 97962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218436 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 979.85 Current children cumulated vsize (Kb) 13796 [startup+990.083 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 98962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218280 134849057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 989.85 Current children cumulated vsize (Kb) 13796 [startup+1000.08 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 99963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218448 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 999.86 Current children cumulated vsize (Kb) 13796 [startup+1010.08 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 100963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218976 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1009.86 Current children cumulated vsize (Kb) 13796 [startup+1020.09 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 101963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219360 134629236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1019.86 Current children cumulated vsize (Kb) 13796 [startup+1030.09 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 102963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219328 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1029.86 Current children cumulated vsize (Kb) 13796 [startup+1040.09 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 103964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219148 134722542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1039.87 Current children cumulated vsize (Kb) 13796 [startup+1050.09 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 104964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218956 134845882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1049.87 Current children cumulated vsize (Kb) 13796 [startup+1060.09 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 105964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219296 134693582 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1059.87 Current children cumulated vsize (Kb) 13796 [startup+1070.09 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 106964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219040 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1069.87 Current children cumulated vsize (Kb) 13796 [startup+1080.09 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 107964 22 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218944 134844637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1079.88 Current children cumulated vsize (Kb) 13796 [startup+1090.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 108964 22 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219364 134629267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1089.88 Current children cumulated vsize (Kb) 13796 [startup+1100.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 109964 22 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219188 134629364 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1099.88 Current children cumulated vsize (Kb) 13796 [startup+1110.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 110964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219352 134522234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1109.89 Current children cumulated vsize (Kb) 13796 [startup+1120.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 111964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219708 134694368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1119.89 Current children cumulated vsize (Kb) 13796 [startup+1130.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 112964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219456 134696608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1129.89 Current children cumulated vsize (Kb) 13796 [startup+1140.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 113964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221220208 134694532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1139.89 Current children cumulated vsize (Kb) 13796 [startup+1150.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 114965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219872 134849108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1149.9 Current children cumulated vsize (Kb) 13796 [startup+1160.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 115965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219716 134629088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1159.9 Current children cumulated vsize (Kb) 13796 [startup+1170.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 116965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219664 134522338 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1169.9 Current children cumulated vsize (Kb) 13796 [startup+1180.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 117965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219932 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1179.9 Current children cumulated vsize (Kb) 13796 [startup+1190.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 118965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219868 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1189.9 Current children cumulated vsize (Kb) 13796 [startup+1200.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 119965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219644 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1199.9 Current children cumulated vsize (Kb) 13796 [startup+1210.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 120966 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219600 134845913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1209.91 Current children cumulated vsize (Kb) 13796 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13397 Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/13392/statm): 532 234 485 147 0 385 0 [pid=13392] vsize: 2128 Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 120966 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219616 134696726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0 [pid=13397] vsize: 11668 Current children cumulated CPU time (s) 1209.91 Current children cumulated vsize (Kb) 13796 Sending SIGTERM to -13392 Sleeping 2 seconds One traced child (pid=13392) ended because it received signal 15 (SIGTERM) One traced child (pid=13397) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.11 CPU time (s): 1209.91 CPU user time (s): 1209.66 CPU system time (s): 0.244962 CPU usage (%): 99.983 Max. virtual memory (cumulated for all children) (Kb): 13796
ERROR: no interpretation found !