Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-rail507.opb |
MD5SUM | 3525728b1c2480586834886de2d50400 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 284672000000000 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 63309 |
Biggest coefficient in the objective function | 53687091200000000000 |
Number of bits for the biggest coefficient in the objective function | 66 |
Sum of the numbers in the objective function | 215947469635884908544 |
Number of bits of the sum of numbers in the objective function | 68 |
Biggest number in a constraint | 53687091200000000000 |
Number of bits of the biggest number in a constraint | 66 |
Biggest sum of numbers in a constraint | 215947469635884908544 |
Number of bits of the biggest sum of numbers | 68 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1234.36 |
Number of variables | 63009 |
Total number of constraints | 63518 |
Number of constraints which are clauses | 507 |
Number of constraints which are cardinality constraints (but not clauses) | 63011 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 59416 |
LAUNCH ON wulflinc12 THE 2005-09-20 02:09:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3111 boxname=wulflinc12 idbench=767 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3525728b1c2480586834886de2d50400 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-rail507.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-rail507.opb IDLAUNCH: 3111 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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.091 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: 902380 kB Buffers: 33112 kB Cached: 68192 kB SwapCached: 492 kB Active: 50192 kB Inactive: 53660 kB HighTotal: 131008 kB HighFree: 60592 kB LowTotal: 903652 kB LowFree: 841788 kB SwapTotal: 2097136 kB SwapFree: 2096072 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5884 kB Slab: 22600 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 02:30:03 (client local time) WITH STATUS 0 IN 1208.33 SECONDS stats: 3111 7 1208.33 0
c Parsing PB file... c PARSE ERROR! [line 63023] 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/9553/stat): 9553 (minisat+_script) R 9552 9553 8263 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796586986 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9553/statm): 174 3 169 147 0 27 0 [pid=9553] 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=9554 New process pid=9555 New process pid=9556 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 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 One traced child (pid=9555) exited with status: 0 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=9556) exited with status: 0 One traced child (pid=9554) exited with status: 0 New process pid=9557 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-rail507.opb One traced child (pid=9557) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=9558 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-rail507.opb [startup+10.0042 s] Raw data (loadavg): 0.88 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 3403 0 0 0 865 24 0 0 25 0 1 0 1796587067 13893632 3202 4294967295 134512640 135167914 3221224448 3221219792 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 3392 3202 162 162 0 3230 0 [pid=9558] vsize: 13568 Current children cumulated CPU time (s) 9.52 Current children cumulated vsize (Kb) 15696 [startup+20.005 s] Raw data (loadavg): 0.90 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 6777 0 0 0 1824 43 0 0 25 0 1 0 1796587067 23515136 5523 4294967295 134512640 135167914 3221224448 3221222848 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9558/statm): 5741 5523 162 162 0 5579 0 [pid=9558] vsize: 22964 Current children cumulated CPU time (s) 19.3 Current children cumulated vsize (Kb) 25092 [startup+30.0049 s] Raw data (loadavg): 0.91 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 11072 0 0 0 2777 67 0 0 25 0 1 0 1796587067 33783808 7985 4294967295 134512640 135167914 3221224448 3221222608 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 8248 7985 162 162 0 8086 0 [pid=9558] vsize: 32992 Current children cumulated CPU time (s) 29.07 Current children cumulated vsize (Kb) 35120 [startup+40.0057 s] Raw data (loadavg): 0.93 0.97 0.99 3/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 16794 0 0 0 3725 92 0 0 25 0 1 0 1796587067 46080000 10992 4294967295 134512640 135167914 3221224448 3220103168 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 11251 10993 162 162 0 11089 0 [pid=9558] vsize: 45000 Current children cumulated CPU time (s) 38.8 Current children cumulated vsize (Kb) 47128 [startup+50.0075 s] Raw data (loadavg): 0.94 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21921 0 0 0 4695 110 0 0 25 0 1 0 1796587067 67084288 16119 4294967295 134512640 135167914 3221224448 3208656064 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9558/statm): 16378 16119 162 162 0 16216 0 [pid=9558] vsize: 65512 Current children cumulated CPU time (s) 48.68 Current children cumulated vsize (Kb) 67640 [startup+60.0094 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21940 0 0 0 5694 111 0 0 25 0 1 0 1796587067 67190784 16138 4294967295 134512640 135167914 3221224448 3208991984 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9558/statm): 16404 16138 162 162 0 16242 0 [pid=9558] vsize: 65616 Current children cumulated CPU time (s) 58.68 Current children cumulated vsize (Kb) 67744 [startup+70.0102 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21984 0 0 0 6693 111 0 0 25 0 1 0 1796587067 67358720 16182 4294967295 134512640 135167914 3221224448 3209242940 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16445 16182 162 162 0 16283 0 [pid=9558] vsize: 65780 Current children cumulated CPU time (s) 68.67 Current children cumulated vsize (Kb) 67908 [startup+80.011 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21987 0 0 0 7694 111 0 0 25 0 1 0 1796587067 67358720 16185 4294967295 134512640 135167914 3221224448 3209452032 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16445 16185 162 162 0 16283 0 [pid=9558] vsize: 65780 Current children cumulated CPU time (s) 78.68 Current children cumulated vsize (Kb) 67908 [startup+90.0119 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21989 0 0 0 8693 111 0 0 25 0 1 0 1796587067 67358720 16187 4294967295 134512640 135167914 3221224448 3209634656 134844676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16445 16187 162 162 0 16283 0 [pid=9558] vsize: 65780 Current children cumulated CPU time (s) 88.67 Current children cumulated vsize (Kb) 67908 [startup+100.012 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22018 0 0 0 9694 111 0 0 25 0 1 0 1796587067 67571712 16216 4294967295 134512640 135167914 3221224448 3209798684 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16497 16216 162 162 0 16335 0 [pid=9558] vsize: 65988 Current children cumulated CPU time (s) 98.68 Current children cumulated vsize (Kb) 68116 [startup+110.013 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22020 0 0 0 10694 111 0 0 25 0 1 0 1796587067 67571712 16218 4294967295 134512640 135167914 3221224448 3209949244 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16497 16218 162 162 0 16335 0 [pid=9558] vsize: 65988 Current children cumulated CPU time (s) 108.68 Current children cumulated vsize (Kb) 68116 [startup+120.013 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22022 0 0 0 11694 111 0 0 25 0 1 0 1796587067 67571712 16220 4294967295 134512640 135167914 3221224448 3210088528 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16497 16220 162 162 0 16335 0 [pid=9558] vsize: 65988 Current children cumulated CPU time (s) 118.68 Current children cumulated vsize (Kb) 68116 [startup+130.013 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22024 0 0 0 12694 111 0 0 25 0 1 0 1796587067 67571712 16222 4294967295 134512640 135167914 3221224448 3210219132 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16497 16222 162 162 0 16335 0 [pid=9558] vsize: 65988 Current children cumulated CPU time (s) 128.68 Current children cumulated vsize (Kb) 68116 [startup+140.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22109 0 0 0 13694 112 0 0 25 0 1 0 1796587067 67915776 16307 4294967295 134512640 135167914 3221224448 3210342112 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16307 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 138.69 Current children cumulated vsize (Kb) 68452 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22111 0 0 0 14694 112 0 0 25 0 1 0 1796587067 67915776 16309 4294967295 134512640 135167914 3221224448 3210459200 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16309 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 148.69 Current children cumulated vsize (Kb) 68452 [startup+160.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22112 0 0 0 15694 112 0 0 25 0 1 0 1796587067 67915776 16310 4294967295 134512640 135167914 3221224448 3210570816 134694444 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16310 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 158.69 Current children cumulated vsize (Kb) 68452 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22114 0 0 0 16695 112 0 0 25 0 1 0 1796587067 67915776 16312 4294967295 134512640 135167914 3221224448 3210677888 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16312 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 168.7 Current children cumulated vsize (Kb) 68452 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22115 0 0 0 17695 112 0 0 25 0 1 0 1796587067 67915776 16313 4294967295 134512640 135167914 3221224448 3210780928 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16313 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 178.7 Current children cumulated vsize (Kb) 68452 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22116 0 0 0 18695 112 0 0 25 0 1 0 1796587067 67915776 16314 4294967295 134512640 135167914 3221224448 3210880208 134624640 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16314 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 188.7 Current children cumulated vsize (Kb) 68452 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22118 0 0 0 19695 112 0 0 25 0 1 0 1796587067 67915776 16316 4294967295 134512640 135167914 3221224448 3210976032 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16316 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 198.7 Current children cumulated vsize (Kb) 68452 [startup+210.019 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22119 0 0 0 20695 112 0 0 25 0 1 0 1796587067 67915776 16317 4294967295 134512640 135167914 3221224448 3211069216 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16317 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 208.7 Current children cumulated vsize (Kb) 68452 [startup+220.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22120 0 0 0 21695 112 0 0 25 0 1 0 1796587067 67915776 16318 4294967295 134512640 135167914 3221224448 3211159472 134849148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16318 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 218.7 Current children cumulated vsize (Kb) 68452 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22121 0 0 0 22696 112 0 0 25 0 1 0 1796587067 67915776 16319 4294967295 134512640 135167914 3221224448 3211247292 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16319 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 228.71 Current children cumulated vsize (Kb) 68452 [startup+240.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22122 0 0 0 23696 112 0 0 25 0 1 0 1796587067 67915776 16320 4294967295 134512640 135167914 3221224448 3211332860 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16581 16320 162 162 0 16419 0 [pid=9558] vsize: 66324 Current children cumulated CPU time (s) 238.71 Current children cumulated vsize (Kb) 68452 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22125 0 0 0 24696 113 0 0 25 0 1 0 1796587067 67923968 16323 4294967295 134512640 135167914 3221224448 3211416192 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16583 16323 162 162 0 16421 0 [pid=9558] vsize: 66332 Current children cumulated CPU time (s) 248.72 Current children cumulated vsize (Kb) 68460 [startup+260.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22129 0 0 0 25696 113 0 0 25 0 1 0 1796587067 67936256 16327 4294967295 134512640 135167914 3221224448 3211497724 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16586 16327 162 162 0 16424 0 [pid=9558] vsize: 66344 Current children cumulated CPU time (s) 258.72 Current children cumulated vsize (Kb) 68472 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22134 0 0 0 26696 113 0 0 25 0 1 0 1796587067 67952640 16332 4294967295 134512640 135167914 3221224448 3211577248 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16590 16332 162 162 0 16428 0 [pid=9558] vsize: 66360 Current children cumulated CPU time (s) 268.72 Current children cumulated vsize (Kb) 68488 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22138 0 0 0 27696 113 0 0 25 0 1 0 1796587067 68161536 16336 4294967295 134512640 135167914 3221224448 3211655188 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16641 16336 162 162 0 16479 0 [pid=9558] vsize: 66564 Current children cumulated CPU time (s) 278.72 Current children cumulated vsize (Kb) 68692 [startup+290.023 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22142 0 0 0 28696 113 0 0 25 0 1 0 1796587067 68173824 16340 4294967295 134512640 135167914 3221224448 3211731380 134849086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16644 16340 162 162 0 16482 0 [pid=9558] vsize: 66576 Current children cumulated CPU time (s) 288.72 Current children cumulated vsize (Kb) 68704 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22146 0 0 0 29696 113 0 0 25 0 1 0 1796587067 68186112 16344 4294967295 134512640 135167914 3221224448 3211806112 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16647 16344 162 162 0 16485 0 [pid=9558] vsize: 66588 Current children cumulated CPU time (s) 298.72 Current children cumulated vsize (Kb) 68716 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22149 0 0 0 30697 113 0 0 25 0 1 0 1796587067 68194304 16347 4294967295 134512640 135167914 3221224448 3211879420 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16649 16347 162 162 0 16487 0 [pid=9558] vsize: 66596 Current children cumulated CPU time (s) 308.73 Current children cumulated vsize (Kb) 68724 [startup+320.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22153 0 0 0 31697 113 0 0 25 0 1 0 1796587067 68206592 16351 4294967295 134512640 135167914 3221224448 3211951264 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16652 16351 162 162 0 16490 0 [pid=9558] vsize: 66608 Current children cumulated CPU time (s) 318.73 Current children cumulated vsize (Kb) 68736 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22158 0 0 0 32697 113 0 0 25 0 1 0 1796587067 68222976 16356 4294967295 134512640 135167914 3221224448 3212021984 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16656 16356 162 162 0 16494 0 [pid=9558] vsize: 66624 Current children cumulated CPU time (s) 328.73 Current children cumulated vsize (Kb) 68752 [startup+340.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22161 0 0 0 33697 113 0 0 25 0 1 0 1796587067 68231168 16359 4294967295 134512640 135167914 3221224448 3212091488 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16658 16359 162 162 0 16496 0 [pid=9558] vsize: 66632 Current children cumulated CPU time (s) 338.73 Current children cumulated vsize (Kb) 68760 [startup+350.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22165 0 0 0 34697 113 0 0 25 0 1 0 1796587067 68243456 16363 4294967295 134512640 135167914 3221224448 3212160096 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16661 16363 162 162 0 16499 0 [pid=9558] vsize: 66644 Current children cumulated CPU time (s) 348.73 Current children cumulated vsize (Kb) 68772 [startup+360.028 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22169 0 0 0 35697 113 0 0 25 0 1 0 1796587067 68255744 16367 4294967295 134512640 135167914 3221224448 3212227296 134694383 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16664 16367 162 162 0 16502 0 [pid=9558] vsize: 66656 Current children cumulated CPU time (s) 358.73 Current children cumulated vsize (Kb) 68784 [startup+370.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22172 0 0 0 36697 113 0 0 25 0 1 0 1796587067 68263936 16370 4294967295 134512640 135167914 3221224448 3212293632 134624644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16666 16370 162 162 0 16504 0 [pid=9558] vsize: 66664 Current children cumulated CPU time (s) 368.73 Current children cumulated vsize (Kb) 68792 [startup+380.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22176 0 0 0 37697 113 0 0 25 0 1 0 1796587067 68276224 16374 4294967295 134512640 135167914 3221224448 3212358736 134843001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16669 16374 162 162 0 16507 0 [pid=9558] vsize: 66676 Current children cumulated CPU time (s) 378.73 Current children cumulated vsize (Kb) 68804 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22178 0 0 0 38697 114 0 0 25 0 1 0 1796587067 68284416 16376 4294967295 134512640 135167914 3221224448 3212423056 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16671 16376 162 162 0 16509 0 [pid=9558] vsize: 66684 Current children cumulated CPU time (s) 388.74 Current children cumulated vsize (Kb) 68812 [startup+400.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22182 0 0 0 39697 114 0 0 25 0 1 0 1796587067 68296704 16380 4294967295 134512640 135167914 3221224448 3212486464 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16674 16380 162 162 0 16512 0 [pid=9558] vsize: 66696 Current children cumulated CPU time (s) 398.74 Current children cumulated vsize (Kb) 68824 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22185 0 0 0 40698 114 0 0 25 0 1 0 1796587067 68304896 16383 4294967295 134512640 135167914 3221224448 3212548956 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16676 16383 162 162 0 16514 0 [pid=9558] vsize: 66704 Current children cumulated CPU time (s) 408.75 Current children cumulated vsize (Kb) 68832 [startup+420.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22189 0 0 0 41698 114 0 0 25 0 1 0 1796587067 68317184 16387 4294967295 134512640 135167914 3221224448 3212610560 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16679 16387 162 162 0 16517 0 [pid=9558] vsize: 66716 Current children cumulated CPU time (s) 418.75 Current children cumulated vsize (Kb) 68844 [startup+430.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22358 0 0 0 42698 114 0 0 25 0 1 0 1796587067 68661248 16472 4294967295 134512640 135167914 3221224448 3212671276 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16763 16472 162 162 0 16601 0 [pid=9558] vsize: 67052 Current children cumulated CPU time (s) 428.75 Current children cumulated vsize (Kb) 69180 [startup+440.034 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22361 0 0 0 43698 114 0 0 25 0 1 0 1796587067 68673536 16475 4294967295 134512640 135167914 3221224448 3212731216 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16766 16475 162 162 0 16604 0 [pid=9558] vsize: 67064 Current children cumulated CPU time (s) 438.75 Current children cumulated vsize (Kb) 69192 [startup+450.034 s] Raw data (loadavg): 0.99 0.97 0.99 3/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22364 0 0 0 44698 114 0 0 25 0 1 0 1796587067 68681728 16478 4294967295 134512640 135167914 3221224448 3212790704 134624604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16768 16478 162 162 0 16606 0 [pid=9558] vsize: 67072 Current children cumulated CPU time (s) 448.75 Current children cumulated vsize (Kb) 69200 [startup+460.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22367 0 0 0 45698 114 0 0 25 0 1 0 1796587067 68689920 16481 4294967295 134512640 135167914 3221224448 3212849312 134722532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16770 16481 162 162 0 16608 0 [pid=9558] vsize: 67080 Current children cumulated CPU time (s) 458.75 Current children cumulated vsize (Kb) 69208 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22371 0 0 0 46698 114 0 0 25 0 1 0 1796587067 68702208 16485 4294967295 134512640 135167914 3221224448 3212907372 134722660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16773 16485 162 162 0 16611 0 [pid=9558] vsize: 67092 Current children cumulated CPU time (s) 468.75 Current children cumulated vsize (Kb) 69220 [startup+480.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22374 0 0 0 47698 115 0 0 25 0 1 0 1796587067 68710400 16488 4294967295 134512640 135167914 3221224448 3212964480 134694407 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16775 16488 162 162 0 16613 0 [pid=9558] vsize: 67100 Current children cumulated CPU time (s) 478.76 Current children cumulated vsize (Kb) 69228 [startup+490.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22376 0 0 0 48699 115 0 0 25 0 1 0 1796587067 68718592 16490 4294967295 134512640 135167914 3221224448 3213021024 134844641 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16777 16490 162 162 0 16615 0 [pid=9558] vsize: 67108 Current children cumulated CPU time (s) 488.77 Current children cumulated vsize (Kb) 69236 [startup+500.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22379 0 0 0 49699 115 0 0 25 0 1 0 1796587067 68726784 16493 4294967295 134512640 135167914 3221224448 3213077024 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16779 16493 162 162 0 16617 0 [pid=9558] vsize: 67116 Current children cumulated CPU time (s) 498.77 Current children cumulated vsize (Kb) 69244 [startup+510.039 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22383 0 0 0 50698 116 0 0 25 0 1 0 1796587067 68739072 16497 4294967295 134512640 135167914 3221224448 3213132444 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16782 16497 162 162 0 16620 0 [pid=9558] vsize: 67128 Current children cumulated CPU time (s) 508.77 Current children cumulated vsize (Kb) 69256 [startup+520.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22384 0 0 0 51697 117 0 0 25 0 1 0 1796587067 68743168 16498 4294967295 134512640 135167914 3221224448 3213187152 134849143 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16783 16498 162 162 0 16621 0 [pid=9558] vsize: 67132 Current children cumulated CPU time (s) 518.77 Current children cumulated vsize (Kb) 69260 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22388 0 0 0 52697 117 0 0 25 0 1 0 1796587067 68755456 16502 4294967295 134512640 135167914 3221224448 3213241056 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16786 16502 162 162 0 16624 0 [pid=9558] vsize: 67144 Current children cumulated CPU time (s) 528.77 Current children cumulated vsize (Kb) 69272 [startup+540.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22391 0 0 0 53697 117 0 0 25 0 1 0 1796587067 68763648 16505 4294967295 134512640 135167914 3221224448 3213294880 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16788 16505 162 162 0 16626 0 [pid=9558] vsize: 67152 Current children cumulated CPU time (s) 538.77 Current children cumulated vsize (Kb) 69280 [startup+550.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22394 0 0 0 54696 117 0 0 25 0 1 0 1796587067 68771840 16508 4294967295 134512640 135167914 3221224448 3213347904 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16790 16508 162 162 0 16628 0 [pid=9558] vsize: 67160 Current children cumulated CPU time (s) 548.76 Current children cumulated vsize (Kb) 69288 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22396 0 0 0 55697 117 0 0 25 0 1 0 1796587067 68780032 16510 4294967295 134512640 135167914 3221224448 3213400588 134845882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16792 16510 162 162 0 16630 0 [pid=9558] vsize: 67168 Current children cumulated CPU time (s) 558.77 Current children cumulated vsize (Kb) 69296 [startup+570.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22399 0 0 0 56697 117 0 0 25 0 1 0 1796587067 68788224 16513 4294967295 134512640 135167914 3221224448 3213452624 134624657 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16794 16513 162 162 0 16632 0 [pid=9558] vsize: 67176 Current children cumulated CPU time (s) 568.77 Current children cumulated vsize (Kb) 69304 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22403 0 0 0 57697 117 0 0 25 0 1 0 1796587067 68800512 16517 4294967295 134512640 135167914 3221224448 3213504076 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16797 16517 162 162 0 16635 0 [pid=9558] vsize: 67188 Current children cumulated CPU time (s) 578.77 Current children cumulated vsize (Kb) 69316 [startup+590.045 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22404 0 0 0 58697 118 0 0 25 0 1 0 1796587067 68804608 16518 4294967295 134512640 135167914 3221224448 3213555392 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16798 16518 162 162 0 16636 0 [pid=9558] vsize: 67192 Current children cumulated CPU time (s) 588.78 Current children cumulated vsize (Kb) 69320 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22407 0 0 0 59697 118 0 0 25 0 1 0 1796587067 68812800 16521 4294967295 134512640 135167914 3221224448 3213605996 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16800 16521 162 162 0 16638 0 [pid=9558] vsize: 67200 Current children cumulated CPU time (s) 598.78 Current children cumulated vsize (Kb) 69328 [startup+610.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22410 0 0 0 60697 118 0 0 25 0 1 0 1796587067 68820992 16524 4294967295 134512640 135167914 3221224448 3213656112 134845895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16802 16524 162 162 0 16640 0 [pid=9558] vsize: 67208 Current children cumulated CPU time (s) 608.78 Current children cumulated vsize (Kb) 69336 [startup+620.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22413 0 0 0 61697 118 0 0 25 0 1 0 1796587067 68833280 16527 4294967295 134512640 135167914 3221224448 3213705892 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16805 16527 162 162 0 16643 0 [pid=9558] vsize: 67220 Current children cumulated CPU time (s) 618.78 Current children cumulated vsize (Kb) 69348 [startup+630.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22415 0 0 0 62698 118 0 0 25 0 1 0 1796587067 68837376 16529 4294967295 134512640 135167914 3221224448 3213755408 134849148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16806 16529 162 162 0 16644 0 [pid=9558] vsize: 67224 Current children cumulated CPU time (s) 628.79 Current children cumulated vsize (Kb) 69352 [startup+640.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22418 0 0 0 63698 118 0 0 25 0 1 0 1796587067 68845568 16532 4294967295 134512640 135167914 3221224448 3213804256 134694398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16808 16532 162 162 0 16646 0 [pid=9558] vsize: 67232 Current children cumulated CPU time (s) 638.79 Current children cumulated vsize (Kb) 69360 [startup+650.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22420 0 0 0 64698 118 0 0 25 0 1 0 1796587067 68853760 16534 4294967295 134512640 135167914 3221224448 3213852912 134624426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16810 16534 162 162 0 16648 0 [pid=9558] vsize: 67240 Current children cumulated CPU time (s) 648.79 Current children cumulated vsize (Kb) 69368 [startup+660.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22423 0 0 0 65698 118 0 0 25 0 1 0 1796587067 68861952 16537 4294967295 134512640 135167914 3221224448 3213900896 134844647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16812 16537 162 162 0 16650 0 [pid=9558] vsize: 67248 Current children cumulated CPU time (s) 658.79 Current children cumulated vsize (Kb) 69376 [startup+670.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22425 0 0 0 66698 118 0 0 25 0 1 0 1796587067 68870144 16539 4294967295 134512640 135167914 3221224448 3213948752 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16814 16539 162 162 0 16652 0 [pid=9558] vsize: 67256 Current children cumulated CPU time (s) 668.79 Current children cumulated vsize (Kb) 69384 [startup+680.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22428 0 0 0 67698 118 0 0 25 0 1 0 1796587067 68878336 16542 4294967295 134512640 135167914 3221224448 3213995904 134844672 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16816 16542 162 162 0 16654 0 [pid=9558] vsize: 67264 Current children cumulated CPU time (s) 678.79 Current children cumulated vsize (Kb) 69392 [startup+690.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22431 0 0 0 68698 119 0 0 25 0 1 0 1796587067 68886528 16545 4294967295 134512640 135167914 3221224448 3214043028 134845938 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16818 16545 162 162 0 16656 0 [pid=9558] vsize: 67272 Current children cumulated CPU time (s) 688.8 Current children cumulated vsize (Kb) 69400 [startup+700.051 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22433 0 0 0 69698 119 0 0 25 0 1 0 1796587067 68894720 16547 4294967295 134512640 135167914 3221224448 3214089656 134694369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16820 16547 162 162 0 16658 0 [pid=9558] vsize: 67280 Current children cumulated CPU time (s) 698.8 Current children cumulated vsize (Kb) 69408 [startup+710.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22435 0 0 0 70698 119 0 0 25 0 1 0 1796587067 68898816 16549 4294967295 134512640 135167914 3221224448 3214135936 134843074 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16821 16549 162 162 0 16659 0 [pid=9558] vsize: 67284 Current children cumulated CPU time (s) 708.8 Current children cumulated vsize (Kb) 69412 [startup+720.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22437 0 0 0 71698 119 0 0 25 0 1 0 1796587067 68907008 16551 4294967295 134512640 135167914 3221224448 3214181920 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16823 16551 162 162 0 16661 0 [pid=9558] vsize: 67292 Current children cumulated CPU time (s) 718.8 Current children cumulated vsize (Kb) 69420 [startup+730.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22440 0 0 0 72699 119 0 0 25 0 1 0 1796587067 68915200 16554 4294967295 134512640 135167914 3221224448 3214227616 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16825 16554 162 162 0 16663 0 [pid=9558] vsize: 67300 Current children cumulated CPU time (s) 728.81 Current children cumulated vsize (Kb) 69428 [startup+740.053 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22443 0 0 0 73698 119 0 0 25 0 1 0 1796587067 68923392 16557 4294967295 134512640 135167914 3221224448 3214272896 134624608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16827 16557 162 162 0 16665 0 [pid=9558] vsize: 67308 Current children cumulated CPU time (s) 738.8 Current children cumulated vsize (Kb) 69436 [startup+750.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22444 0 0 0 74699 119 0 0 25 0 1 0 1796587067 68927488 16558 4294967295 134512640 135167914 3221224448 3214317664 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16828 16558 162 162 0 16666 0 [pid=9558] vsize: 67312 Current children cumulated CPU time (s) 748.81 Current children cumulated vsize (Kb) 69440 [startup+760.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22447 0 0 0 75699 119 0 0 25 0 1 0 1796587067 68935680 16561 4294967295 134512640 135167914 3221224448 3214362176 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16830 16561 162 162 0 16668 0 [pid=9558] vsize: 67320 Current children cumulated CPU time (s) 758.81 Current children cumulated vsize (Kb) 69448 [startup+770.056 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22449 0 0 0 76699 119 0 0 25 0 1 0 1796587067 68943872 16563 4294967295 134512640 135167914 3221224448 3214406564 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16832 16563 162 162 0 16670 0 [pid=9558] vsize: 67328 Current children cumulated CPU time (s) 768.81 Current children cumulated vsize (Kb) 69456 [startup+780.056 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22452 0 0 0 77699 119 0 0 25 0 1 0 1796587067 68952064 16566 4294967295 134512640 135167914 3221224448 3214450644 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16834 16566 162 162 0 16672 0 [pid=9558] vsize: 67336 Current children cumulated CPU time (s) 778.81 Current children cumulated vsize (Kb) 69464 [startup+790.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22455 0 0 0 78699 120 0 0 25 0 1 0 1796587067 68960256 16569 4294967295 134512640 135167914 3221224448 3214494420 134843000 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16836 16569 162 162 0 16674 0 [pid=9558] vsize: 67344 Current children cumulated CPU time (s) 788.82 Current children cumulated vsize (Kb) 69472 [startup+800.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22456 0 0 0 79699 120 0 0 25 0 1 0 1796587067 68964352 16570 4294967295 134512640 135167914 3221224448 3214537648 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16837 16570 162 162 0 16675 0 [pid=9558] vsize: 67348 Current children cumulated CPU time (s) 798.82 Current children cumulated vsize (Kb) 69476 [startup+810.059 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22459 0 0 0 80700 120 0 0 25 0 1 0 1796587067 68972544 16573 4294967295 134512640 135167914 3221224448 3214580736 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16839 16573 162 162 0 16677 0 [pid=9558] vsize: 67356 Current children cumulated CPU time (s) 808.83 Current children cumulated vsize (Kb) 69484 [startup+820.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22461 0 0 0 81700 120 0 0 25 0 1 0 1796587067 68980736 16575 4294967295 134512640 135167914 3221224448 3214623648 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16841 16575 162 162 0 16679 0 [pid=9558] vsize: 67364 Current children cumulated CPU time (s) 818.83 Current children cumulated vsize (Kb) 69492 [startup+830.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22464 0 0 0 82700 120 0 0 25 0 1 0 1796587067 68988928 16578 4294967295 134512640 135167914 3221224448 3214666256 134624724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16843 16578 162 162 0 16681 0 [pid=9558] vsize: 67372 Current children cumulated CPU time (s) 828.83 Current children cumulated vsize (Kb) 69500 [startup+840.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22465 0 0 0 83700 120 0 0 25 0 1 0 1796587067 68993024 16579 4294967295 134512640 135167914 3221224448 3214708544 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16844 16579 162 162 0 16682 0 [pid=9558] vsize: 67376 Current children cumulated CPU time (s) 838.83 Current children cumulated vsize (Kb) 69504 [startup+850.061 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22468 0 0 0 84700 120 0 0 25 0 1 0 1796587067 69001216 16582 4294967295 134512640 135167914 3221224448 3214750656 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16846 16582 162 162 0 16684 0 [pid=9558] vsize: 67384 Current children cumulated CPU time (s) 848.83 Current children cumulated vsize (Kb) 69512 [startup+860.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22470 0 0 0 85701 120 0 0 25 0 1 0 1796587067 69009408 16584 4294967295 134512640 135167914 3221224448 3214792352 134624782 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16848 16584 162 162 0 16686 0 [pid=9558] vsize: 67392 Current children cumulated CPU time (s) 858.84 Current children cumulated vsize (Kb) 69520 [startup+870.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22472 0 0 0 86701 120 0 0 25 0 1 0 1796587067 69013504 16586 4294967295 134512640 135167914 3221224448 3214833980 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16849 16586 162 162 0 16687 0 [pid=9558] vsize: 67396 Current children cumulated CPU time (s) 868.84 Current children cumulated vsize (Kb) 69524 [startup+880.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22475 0 0 0 87701 120 0 0 25 0 1 0 1796587067 69021696 16589 4294967295 134512640 135167914 3221224448 3214875196 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16851 16589 162 162 0 16689 0 [pid=9558] vsize: 67404 Current children cumulated CPU time (s) 878.84 Current children cumulated vsize (Kb) 69532 [startup+890.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22476 0 0 0 88701 120 0 0 25 0 1 0 1796587067 69025792 16590 4294967295 134512640 135167914 3221224448 3214916064 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16852 16590 162 162 0 16690 0 [pid=9558] vsize: 67408 Current children cumulated CPU time (s) 888.84 Current children cumulated vsize (Kb) 69536 [startup+900.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22479 0 0 0 89701 120 0 0 25 0 1 0 1796587067 69033984 16593 4294967295 134512640 135167914 3221224448 3214956860 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16854 16593 162 162 0 16692 0 [pid=9558] vsize: 67416 Current children cumulated CPU time (s) 898.84 Current children cumulated vsize (Kb) 69544 [startup+910.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22481 0 0 0 90702 120 0 0 25 0 1 0 1796587067 69042176 16595 4294967295 134512640 135167914 3221224448 3214997440 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16856 16595 162 162 0 16694 0 [pid=9558] vsize: 67424 Current children cumulated CPU time (s) 908.85 Current children cumulated vsize (Kb) 69552 [startup+920.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22484 0 0 0 91702 120 0 0 25 0 1 0 1796587067 69050368 16598 4294967295 134512640 135167914 3221224448 3215037872 134624420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16858 16598 162 162 0 16696 0 [pid=9558] vsize: 67432 Current children cumulated CPU time (s) 918.85 Current children cumulated vsize (Kb) 69560 [startup+930.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22485 0 0 0 92702 120 0 0 25 0 1 0 1796587067 69054464 16599 4294967295 134512640 135167914 3221224448 3215077856 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16859 16599 162 162 0 16697 0 [pid=9558] vsize: 67436 Current children cumulated CPU time (s) 928.85 Current children cumulated vsize (Kb) 69564 [startup+940.069 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22487 0 0 0 93702 120 0 0 25 0 1 0 1796587067 69058560 16601 4294967295 134512640 135167914 3221224448 3215117832 134624744 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16860 16601 162 162 0 16698 0 [pid=9558] vsize: 67440 Current children cumulated CPU time (s) 938.85 Current children cumulated vsize (Kb) 69568 [startup+950.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22489 0 0 0 94703 120 0 0 25 0 1 0 1796587067 69066752 16603 4294967295 134512640 135167914 3221224448 3215157404 134845882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16862 16603 162 162 0 16700 0 [pid=9558] vsize: 67448 Current children cumulated CPU time (s) 948.86 Current children cumulated vsize (Kb) 69576 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22492 0 0 0 95703 120 0 0 25 0 1 0 1796587067 69074944 16606 4294967295 134512640 135167914 3221224448 3215196864 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16864 16606 162 162 0 16702 0 [pid=9558] vsize: 67456 Current children cumulated CPU time (s) 958.86 Current children cumulated vsize (Kb) 69584 [startup+970.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22494 0 0 0 96703 120 0 0 25 0 1 0 1796587067 69083136 16608 4294967295 134512640 135167914 3221224448 3215236080 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16866 16608 162 162 0 16704 0 [pid=9558] vsize: 67464 Current children cumulated CPU time (s) 968.86 Current children cumulated vsize (Kb) 69592 [startup+980.073 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22495 0 0 0 97703 120 0 0 25 0 1 0 1796587067 69476352 16609 4294967295 134512640 135167914 3221224448 3215274988 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16962 16609 162 162 0 16800 0 [pid=9558] vsize: 67848 Current children cumulated CPU time (s) 978.86 Current children cumulated vsize (Kb) 69976 [startup+990.074 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22497 0 0 0 98703 121 0 0 25 0 1 0 1796587067 69484544 16611 4294967295 134512640 135167914 3221224448 3215313788 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16964 16611 162 162 0 16802 0 [pid=9558] vsize: 67856 Current children cumulated CPU time (s) 988.87 Current children cumulated vsize (Kb) 69984 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22500 0 0 0 99703 121 0 0 25 0 1 0 1796587067 69492736 16614 4294967295 134512640 135167914 3221224448 3215352368 134624410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16966 16614 162 162 0 16804 0 [pid=9558] vsize: 67864 Current children cumulated CPU time (s) 998.87 Current children cumulated vsize (Kb) 69992 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22502 0 0 0 100703 121 0 0 25 0 1 0 1796587067 69500928 16616 4294967295 134512640 135167914 3221224448 3215390848 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16968 16616 162 162 0 16806 0 [pid=9558] vsize: 67872 Current children cumulated CPU time (s) 1008.87 Current children cumulated vsize (Kb) 70000 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22504 0 0 0 101704 121 0 0 25 0 1 0 1796587067 69505024 16618 4294967295 134512640 135167914 3221224448 3215428928 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16969 16618 162 162 0 16807 0 [pid=9558] vsize: 67876 Current children cumulated CPU time (s) 1018.88 Current children cumulated vsize (Kb) 70004 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22505 0 0 0 102704 121 0 0 25 0 1 0 1796587067 69509120 16619 4294967295 134512640 135167914 3221224448 3215466944 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16970 16619 162 162 0 16808 0 [pid=9558] vsize: 67880 Current children cumulated CPU time (s) 1028.88 Current children cumulated vsize (Kb) 70008 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22508 0 0 0 103704 121 0 0 25 0 1 0 1796587067 69517312 16622 4294967295 134512640 135167914 3221224448 3215504640 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16972 16622 162 162 0 16810 0 [pid=9558] vsize: 67888 Current children cumulated CPU time (s) 1038.88 Current children cumulated vsize (Kb) 70016 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22509 0 0 0 104704 121 0 0 25 0 1 0 1796587067 69521408 16623 4294967295 134512640 135167914 3221224448 3215542288 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16973 16623 162 162 0 16811 0 [pid=9558] vsize: 67892 Current children cumulated CPU time (s) 1048.88 Current children cumulated vsize (Kb) 70020 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22512 0 0 0 105704 121 0 0 25 0 1 0 1796587067 69529600 16626 4294967295 134512640 135167914 3221224448 3215579616 134843074 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16975 16626 162 162 0 16813 0 [pid=9558] vsize: 67900 Current children cumulated CPU time (s) 1058.88 Current children cumulated vsize (Kb) 70028 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22514 0 0 0 106705 121 0 0 25 0 1 0 1796587067 69537792 16628 4294967295 134512640 135167914 3221224448 3215616736 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16977 16628 162 162 0 16815 0 [pid=9558] vsize: 67908 Current children cumulated CPU time (s) 1068.89 Current children cumulated vsize (Kb) 70036 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22515 0 0 0 107705 121 0 0 25 0 1 0 1796587067 69537792 16629 4294967295 134512640 135167914 3221224448 3215654096 134624420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16977 16629 162 162 0 16815 0 [pid=9558] vsize: 67908 Current children cumulated CPU time (s) 1078.89 Current children cumulated vsize (Kb) 70036 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22517 0 0 0 108705 121 0 0 25 0 1 0 1796587067 69545984 16631 4294967295 134512640 135167914 3221224448 3215690796 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16979 16631 162 162 0 16817 0 [pid=9558] vsize: 67916 Current children cumulated CPU time (s) 1088.89 Current children cumulated vsize (Kb) 70044 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22520 0 0 0 109705 121 0 0 25 0 1 0 1796587067 69554176 16634 4294967295 134512640 135167914 3221224448 3215727516 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16981 16634 162 162 0 16819 0 [pid=9558] vsize: 67924 Current children cumulated CPU time (s) 1098.89 Current children cumulated vsize (Kb) 70052 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22521 0 0 0 110704 122 0 0 25 0 1 0 1796587067 69558272 16635 4294967295 134512640 135167914 3221224448 3215764016 134849148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16982 16635 162 162 0 16820 0 [pid=9558] vsize: 67928 Current children cumulated CPU time (s) 1108.89 Current children cumulated vsize (Kb) 70056 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22524 0 0 0 111704 123 0 0 25 0 1 0 1796587067 69566464 16638 4294967295 134512640 135167914 3221224448 3215800220 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16984 16638 162 162 0 16822 0 [pid=9558] vsize: 67936 Current children cumulated CPU time (s) 1118.9 Current children cumulated vsize (Kb) 70064 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22525 0 0 0 112704 123 0 0 25 0 1 0 1796587067 69570560 16639 4294967295 134512640 135167914 3221224448 3215836392 134722657 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16985 16639 162 162 0 16823 0 [pid=9558] vsize: 67940 Current children cumulated CPU time (s) 1128.9 Current children cumulated vsize (Kb) 70068 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22527 0 0 0 113704 123 0 0 25 0 1 0 1796587067 69574656 16641 4294967295 134512640 135167914 3221224448 3215872496 134624420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16986 16641 162 162 0 16824 0 [pid=9558] vsize: 67944 Current children cumulated CPU time (s) 1138.9 Current children cumulated vsize (Kb) 70072 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22529 0 0 0 114704 124 0 0 25 0 1 0 1796587067 69582848 16643 4294967295 134512640 135167914 3221224448 3215908236 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16988 16643 162 162 0 16826 0 [pid=9558] vsize: 67952 Current children cumulated CPU time (s) 1148.91 Current children cumulated vsize (Kb) 70080 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22532 0 0 0 115704 124 0 0 25 0 1 0 1796587067 69591040 16646 4294967295 134512640 135167914 3221224448 3215943904 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16990 16646 162 162 0 16828 0 [pid=9558] vsize: 67960 Current children cumulated CPU time (s) 1158.91 Current children cumulated vsize (Kb) 70088 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22533 0 0 0 116704 124 0 0 25 0 1 0 1796587067 69595136 16647 4294967295 134512640 135167914 3221224448 3215979520 134694444 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16991 16647 162 162 0 16829 0 [pid=9558] vsize: 67964 Current children cumulated CPU time (s) 1168.91 Current children cumulated vsize (Kb) 70092 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22534 0 0 0 117704 124 0 0 25 0 1 0 1796587067 69599232 16648 4294967295 134512640 135167914 3221224448 3216014928 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16992 16648 162 162 0 16830 0 [pid=9558] vsize: 67968 Current children cumulated CPU time (s) 1178.91 Current children cumulated vsize (Kb) 70096 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22536 0 0 0 118704 124 0 0 25 0 1 0 1796587067 69603328 16650 4294967295 134512640 135167914 3221224448 3216050108 134849088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16993 16650 162 162 0 16831 0 [pid=9558] vsize: 67972 Current children cumulated CPU time (s) 1188.91 Current children cumulated vsize (Kb) 70100 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22538 0 0 0 119704 124 0 0 25 0 1 0 1796587067 69611520 16652 4294967295 134512640 135167914 3221224448 3216084960 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16995 16652 162 162 0 16833 0 [pid=9558] vsize: 67980 Current children cumulated CPU time (s) 1198.91 Current children cumulated vsize (Kb) 70108 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22540 0 0 0 120704 124 0 0 25 0 1 0 1796587067 69615616 16654 4294967295 134512640 135167914 3221224448 3216120000 134624613 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16996 16654 162 162 0 16834 0 [pid=9558] vsize: 67984 Current children cumulated CPU time (s) 1208.91 Current children cumulated vsize (Kb) 70112 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 9558 Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9553/statm): 532 234 485 147 0 385 0 [pid=9553] vsize: 2128 Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22540 0 0 0 120705 124 0 0 25 0 1 0 1796587067 69615616 16654 4294967295 134512640 135167914 3221224448 3216119964 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9558/statm): 16996 16654 162 162 0 16834 0 [pid=9558] vsize: 67984 Current children cumulated CPU time (s) 1208.92 Current children cumulated vsize (Kb) 70112 Sending SIGTERM to -9553 Sleeping 2 seconds One traced child (pid=9553) ended because it received signal 15 (SIGTERM) One traced child (pid=9558) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.12 CPU time (s): 1208.33 CPU user time (s): 1207.05 CPU system time (s): 1.27981 CPU usage (%): 99.8517 Max. virtual memory (cumulated for all children) (Kb): 70112
ERROR: no interpretation found !