Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-blend2.opb |
MD5SUM | 16b86ac5ad712621c8050f8776cfb803 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 88 |
Biggest coefficient in the objective function | 24014225 |
Number of bits for the biggest coefficient in the objective function | 25 |
Sum of the numbers in the objective function | 235593725 |
Number of bits of the sum of numbers in the objective function | 28 |
Biggest number in a constraint | 8935312239624192 |
Number of bits of the biggest number in a constraint | 53 |
Biggest sum of numbers in a constraint | 1346963845029350184 |
Number of bits of the biggest sum of numbers | 61 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2944 |
Total number of constraints | 531 |
Number of constraints which are clauses | 9 |
Number of constraints which are cardinality constraints (but not clauses) | 310 |
Number of constraints which are nor clauses,nor cardinality constraints | 212 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2659 |
LAUNCH ON wulflinc29 THE 2005-09-19 17:45:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2963 boxname=wulflinc29 idbench=619 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 16b86ac5ad712621c8050f8776cfb803 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-blend2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-blend2.opb IDLAUNCH: 2963 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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: 841108 kB Buffers: 34944 kB Cached: 129232 kB SwapCached: 792 kB Active: 64756 kB Inactive: 102052 kB HighTotal: 131008 kB HighFree: 44912 kB LowTotal: 903652 kB LowFree: 796196 kB SwapTotal: 2097892 kB SwapFree: 2096664 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5744 kB Slab: 21208 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 17:56:41 (client local time) WITH STATUS 0 IN 659.449 SECONDS stats: 2963 7 659.449 0
c Parsing PB file... c PARSE ERROR! [line 702] 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/30214/stat): 30214 (minisat+_script) R 30213 30214 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1851789152 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/30214/statm): 174 3 169 147 0 27 0 [pid=30214] 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=30215 New process pid=30216 New process pid=30217 execve syscall for /bin/sed executable One traced child (pid=30216) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=30217) exited with status: 0 One traced child (pid=30215) exited with status: 0 New process pid=30218 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-blend2.opb One traced child (pid=30218) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=30219 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-blend2.opb [startup+10.0052 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 4820 0 3 0 926 20 0 0 25 0 1 0 1851789180 17432576 4106 4294967295 134512640 135167914 3221224448 3220804600 134619943 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 4256 4106 162 162 0 4094 0 [pid=30219] vsize: 17024 Current children cumulated CPU time (s) 9.55 Current children cumulated vsize (Kb) 19152 [startup+20.006 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 11198 0 3 0 1866 48 0 0 25 0 1 0 1851789180 40857600 9825 4294967295 134512640 135167914 3221224448 3220805968 134620274 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 9975 9825 162 162 0 9813 0 [pid=30219] vsize: 39900 Current children cumulated CPU time (s) 19.23 Current children cumulated vsize (Kb) 42028 [startup+30.0068 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 18459 0 3 0 2808 77 0 0 25 0 1 0 1851789180 65200128 15768 4294967295 134512640 135167914 3221224448 3220807292 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 15918 15768 162 162 0 15756 0 [pid=30219] vsize: 63672 Current children cumulated CPU time (s) 28.94 Current children cumulated vsize (Kb) 65800 [startup+40.0076 s] Raw data (loadavg): 0.99 0.97 0.71 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 27826 0 3 0 3754 107 0 0 25 0 1 0 1851789180 103567360 25135 4294967295 134512640 135167914 3221224448 3220806896 134844647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 25285 25135 162 162 0 25123 0 [pid=30219] vsize: 101140 Current children cumulated CPU time (s) 38.7 Current children cumulated vsize (Kb) 103268 [startup+50.0094 s] Raw data (loadavg): 0.99 0.97 0.71 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 32665 0 3 0 4704 129 0 0 25 0 1 0 1851789180 112586752 27337 4294967295 134512640 135167914 3221224448 3220810528 134694386 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 27487 27337 162 162 0 27325 0 [pid=30219] vsize: 109948 Current children cumulated CPU time (s) 48.42 Current children cumulated vsize (Kb) 112076 [startup+60.0102 s] Raw data (loadavg): 0.99 0.97 0.71 1/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 37450 0 3 0 5655 151 0 0 25 0 1 0 1851789180 132186112 32122 4294967295 134512640 135167914 3221224448 3220804124 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 32272 32122 162 162 0 32110 0 [pid=30219] vsize: 129088 Current children cumulated CPU time (s) 58.15 Current children cumulated vsize (Kb) 131216 [startup+70.0109 s] Raw data (loadavg): 0.99 0.97 0.72 1/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 41956 0 3 0 6611 170 0 0 25 0 1 0 1851789180 150642688 36628 4294967295 134512640 135167914 3221224448 3220806684 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 36778 36628 162 162 0 36616 0 [pid=30219] vsize: 147112 Current children cumulated CPU time (s) 67.9 Current children cumulated vsize (Kb) 149240 [startup+80.0118 s] Raw data (loadavg): 0.99 0.97 0.72 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 55168 0 3 0 7553 210 0 0 25 0 1 0 1851789180 183160832 44567 4294967295 134512640 135167914 3221224448 3220814592 134843064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 44717 44567 162 162 0 44555 0 [pid=30219] vsize: 178868 Current children cumulated CPU time (s) 77.72 Current children cumulated vsize (Kb) 180996 [startup+90.0125 s] Raw data (loadavg): 0.99 0.97 0.72 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 59409 0 3 0 8504 230 0 0 25 0 1 0 1851789180 200531968 48808 4294967295 134512640 135167914 3221224448 3220804400 134621344 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 48958 48808 162 162 0 48796 0 [pid=30219] vsize: 195832 Current children cumulated CPU time (s) 87.43 Current children cumulated vsize (Kb) 197960 [startup+100.013 s] Raw data (loadavg): 0.99 0.97 0.72 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 63473 0 3 0 9462 247 0 0 25 0 1 0 1851789180 217178112 52872 4294967295 134512640 135167914 3221224448 3220810448 134620938 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 53022 52872 162 162 0 52860 0 [pid=30219] vsize: 212088 Current children cumulated CPU time (s) 97.18 Current children cumulated vsize (Kb) 214216 [startup+110.014 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 67408 0 3 0 10420 264 0 0 25 0 1 0 1851789180 233295872 56807 4294967295 134512640 135167914 3221224448 3220804288 134624000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 56957 56807 162 162 0 56795 0 [pid=30219] vsize: 227828 Current children cumulated CPU time (s) 106.93 Current children cumulated vsize (Kb) 229956 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 71242 0 3 0 11376 283 0 0 23 0 1 0 1851789180 248999936 60641 4294967295 134512640 135167914 3221224448 3220812800 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 60791 60641 162 162 0 60629 0 [pid=30219] vsize: 243164 Current children cumulated CPU time (s) 116.68 Current children cumulated vsize (Kb) 245292 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 74893 0 3 0 12337 299 0 0 25 0 1 0 1851789180 263954432 64292 4294967295 134512640 135167914 3221224448 3220806400 134847156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 64442 64292 162 162 0 64280 0 [pid=30219] vsize: 257768 Current children cumulated CPU time (s) 126.45 Current children cumulated vsize (Kb) 259896 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 78608 0 3 0 13302 314 0 0 25 0 1 0 1851789180 279171072 68007 4294967295 134512640 135167914 3221224448 3220807744 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 68157 68007 162 162 0 67995 0 [pid=30219] vsize: 272628 Current children cumulated CPU time (s) 136.25 Current children cumulated vsize (Kb) 274756 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 82124 0 3 0 14262 330 0 0 23 0 1 0 1851789180 293572608 71523 4294967295 134512640 135167914 3221224448 3220818176 134844650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 71673 71523 162 162 0 71511 0 [pid=30219] vsize: 286692 Current children cumulated CPU time (s) 146.01 Current children cumulated vsize (Kb) 288820 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 85469 0 3 0 15229 343 0 0 21 0 1 0 1851789180 307273728 74868 4294967295 134512640 135167914 3221224448 3220804720 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 75018 74868 162 162 0 74856 0 [pid=30219] vsize: 300072 Current children cumulated CPU time (s) 155.81 Current children cumulated vsize (Kb) 302200 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 107269 0 3 0 16171 395 0 0 25 0 1 0 1851789180 353370112 86122 4294967295 134512640 135167914 3221224448 3220803964 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 86272 86122 162 162 0 86110 0 [pid=30219] vsize: 345088 Current children cumulated CPU time (s) 165.75 Current children cumulated vsize (Kb) 347216 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 110659 0 3 0 17133 410 0 0 25 0 1 0 1851789180 367255552 89512 4294967295 134512640 135167914 3221224448 3220806968 134849057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 89662 89512 162 162 0 89500 0 [pid=30219] vsize: 358648 Current children cumulated CPU time (s) 175.52 Current children cumulated vsize (Kb) 360776 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 113896 0 3 0 18098 425 0 0 25 0 1 0 1851789180 380514304 92749 4294967295 134512640 135167914 3221224448 3220807776 134843026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 92899 92749 162 162 0 92737 0 [pid=30219] vsize: 371596 Current children cumulated CPU time (s) 185.32 Current children cumulated vsize (Kb) 373724 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.75 1/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 117050 0 3 0 19062 439 0 0 25 0 1 0 1851789180 393437184 95903 4294967295 134512640 135167914 3221224448 3220803964 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 96054 95903 162 162 0 95892 0 [pid=30219] vsize: 384216 Current children cumulated CPU time (s) 195.1 Current children cumulated vsize (Kb) 386344 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 120260 0 3 0 20027 452 0 0 25 0 1 0 1851789180 406581248 99113 4294967295 134512640 135167914 3221224448 3220810640 134693573 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 99263 99113 162 162 0 99101 0 [pid=30219] vsize: 397052 Current children cumulated CPU time (s) 204.88 Current children cumulated vsize (Kb) 399180 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 123260 0 3 0 20995 466 0 0 25 0 1 0 1851789180 418869248 102113 4294967295 134512640 135167914 3221224448 3220804720 134693561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 102263 102113 162 162 0 102101 0 [pid=30219] vsize: 409052 Current children cumulated CPU time (s) 214.7 Current children cumulated vsize (Kb) 411180 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 126418 0 3 0 21959 481 0 0 25 0 1 0 1851789180 431804416 105271 4294967295 134512640 135167914 3221224448 3220809880 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 105421 105271 162 162 0 105259 0 [pid=30219] vsize: 421684 Current children cumulated CPU time (s) 224.49 Current children cumulated vsize (Kb) 423812 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 129295 0 3 0 22929 494 0 0 25 0 1 0 1851789180 443588608 108148 4294967295 134512640 135167914 3221224448 3220806736 134849082 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 108298 108148 162 162 0 108136 0 [pid=30219] vsize: 433192 Current children cumulated CPU time (s) 234.32 Current children cumulated vsize (Kb) 435320 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 132199 0 3 0 23897 507 0 0 25 0 1 0 1851789180 455483392 111052 4294967295 134512640 135167914 3221224448 3220808732 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 111202 111052 162 162 0 111040 0 [pid=30219] vsize: 444808 Current children cumulated CPU time (s) 244.13 Current children cumulated vsize (Kb) 446936 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 135343 0 3 0 24862 522 0 0 25 0 1 0 1851789180 468361216 114196 4294967295 134512640 135167914 3221224448 3220809072 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 114346 114196 162 162 0 114184 0 [pid=30219] vsize: 457384 Current children cumulated CPU time (s) 253.93 Current children cumulated vsize (Kb) 459512 [startup+270.026 s] Raw data (loadavg): 1.07 0.99 0.76 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 137917 0 3 0 25837 533 0 0 25 0 1 0 1851789180 478904320 116770 4294967295 134512640 135167914 3221224448 3220810540 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 116920 116770 162 162 0 116758 0 [pid=30219] vsize: 467680 Current children cumulated CPU time (s) 263.79 Current children cumulated vsize (Kb) 469808 [startup+280.027 s] Raw data (loadavg): 1.06 0.99 0.77 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 140811 0 3 0 26807 543 0 0 25 0 1 0 1851789180 490758144 119664 4294967295 134512640 135167914 3221224448 3220804416 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 119814 119664 162 162 0 119652 0 [pid=30219] vsize: 479256 Current children cumulated CPU time (s) 273.59 Current children cumulated vsize (Kb) 481384 [startup+290.028 s] Raw data (loadavg): 1.05 0.99 0.77 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 143828 0 3 0 27774 556 0 0 25 0 1 0 1851789180 503115776 122681 4294967295 134512640 135167914 3221224448 3220805648 134843139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 122831 122681 162 162 0 122669 0 [pid=30219] vsize: 491324 Current children cumulated CPU time (s) 283.39 Current children cumulated vsize (Kb) 493452 [startup+300.028 s] Raw data (loadavg): 1.04 0.99 0.77 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 146335 0 3 0 28746 568 0 0 25 0 1 0 1851789180 513380352 125188 4294967295 134512640 135167914 3221224448 3220805472 134843406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 125337 125188 162 162 0 125175 0 [pid=30219] vsize: 501348 Current children cumulated CPU time (s) 293.23 Current children cumulated vsize (Kb) 503476 [startup+310.029 s] Raw data (loadavg): 1.03 0.99 0.77 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 149089 0 3 0 29718 580 0 0 25 0 1 0 1851789180 524660736 127942 4294967295 134512640 135167914 3221224448 3220807024 134522492 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 128091 127942 162 162 0 127929 0 [pid=30219] vsize: 512364 Current children cumulated CPU time (s) 303.07 Current children cumulated vsize (Kb) 514492 [startup+320.029 s] Raw data (loadavg): 1.03 0.99 0.77 1/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 152069 0 3 0 30685 593 0 0 25 0 1 0 1851789180 536858624 130922 4294967295 134512640 135167914 3221224448 3220804796 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 131069 130922 162 162 0 130907 0 [pid=30219] vsize: 524276 Current children cumulated CPU time (s) 312.87 Current children cumulated vsize (Kb) 526404 [startup+330.03 s] Raw data (loadavg): 1.02 0.99 0.78 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 154469 0 3 0 31657 604 0 0 25 0 1 0 1851789180 546684928 133322 4294967295 134512640 135167914 3221224448 3220805848 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 133468 133322 162 162 0 133306 0 [pid=30219] vsize: 533872 Current children cumulated CPU time (s) 322.7 Current children cumulated vsize (Kb) 536000 [startup+340.03 s] Raw data (loadavg): 1.02 0.99 0.78 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 156996 0 3 0 32630 616 0 0 25 0 1 0 1851789180 557035520 135849 4294967295 134512640 135167914 3221224448 3220807136 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 135995 135849 162 162 0 135833 0 [pid=30219] vsize: 543980 Current children cumulated CPU time (s) 332.55 Current children cumulated vsize (Kb) 546108 [startup+350.031 s] Raw data (loadavg): 1.02 0.99 0.78 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 159997 0 3 0 33598 632 0 0 25 0 1 0 1851789180 569319424 138850 4294967295 134512640 135167914 3221224448 3220814200 134845939 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 138994 138850 162 162 0 138832 0 [pid=30219] vsize: 555976 Current children cumulated CPU time (s) 342.39 Current children cumulated vsize (Kb) 558104 [startup+360.031 s] Raw data (loadavg): 1.01 0.99 0.78 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 162473 0 3 0 34571 643 0 0 25 0 1 0 1851789180 579457024 141326 4294967295 134512640 135167914 3221224448 3220804960 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 141469 141326 162 162 0 141307 0 [pid=30219] vsize: 565876 Current children cumulated CPU time (s) 352.23 Current children cumulated vsize (Kb) 568004 [startup+370.031 s] Raw data (loadavg): 1.01 0.99 0.78 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 164787 0 3 0 35547 653 0 0 25 0 1 0 1851789180 588935168 143640 4294967295 134512640 135167914 3221224448 3220805572 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 143783 143640 162 162 0 143621 0 [pid=30219] vsize: 575132 Current children cumulated CPU time (s) 362.09 Current children cumulated vsize (Kb) 577260 [startup+380.032 s] Raw data (loadavg): 1.01 0.99 0.79 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 167703 0 3 0 36516 666 0 0 25 0 1 0 1851789180 600870912 146556 4294967295 134512640 135167914 3221224448 3220806144 134844723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 146697 146556 162 162 0 146535 0 [pid=30219] vsize: 586788 Current children cumulated CPU time (s) 371.91 Current children cumulated vsize (Kb) 588916 [startup+390.032 s] Raw data (loadavg): 1.01 0.99 0.79 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 170258 0 3 0 37488 676 0 0 25 0 1 0 1851789180 611332096 149111 4294967295 134512640 135167914 3221224448 3220805168 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 149251 149111 162 162 0 149089 0 [pid=30219] vsize: 597004 Current children cumulated CPU time (s) 381.73 Current children cumulated vsize (Kb) 599132 [startup+400.034 s] Raw data (loadavg): 1.00 0.99 0.79 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 212960 0 3 0 38385 776 0 0 25 0 1 0 1851789180 786239488 191813 4294967295 134512640 135167914 3221224448 3220803824 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 191953 191813 162 162 0 191791 0 [pid=30219] vsize: 767812 Current children cumulated CPU time (s) 391.7 Current children cumulated vsize (Kb) 769940 [startup+410.036 s] Raw data (loadavg): 1.00 0.99 0.79 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 213371 0 3 0 39377 781 0 0 25 0 1 0 1851789180 701534208 171133 4294967295 134512640 135167914 3221224448 3220804032 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 171273 171133 162 162 0 171111 0 [pid=30219] vsize: 685092 Current children cumulated CPU time (s) 401.67 Current children cumulated vsize (Kb) 687220 [startup+420.036 s] Raw data (loadavg): 1.00 0.99 0.79 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 215603 0 3 0 40352 791 0 0 25 0 1 0 1851789180 710676480 173365 4294967295 134512640 135167914 3221224448 3220804576 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 173505 173365 162 162 0 173343 0 [pid=30219] vsize: 694020 Current children cumulated CPU time (s) 411.52 Current children cumulated vsize (Kb) 696148 [startup+430.037 s] Raw data (loadavg): 1.00 0.99 0.80 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 218304 0 3 0 41323 803 0 0 25 0 1 0 1851789180 721739776 176066 4294967295 134512640 135167914 3221224448 3220808104 134693624 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 176206 176066 162 162 0 176044 0 [pid=30219] vsize: 704824 Current children cumulated CPU time (s) 421.35 Current children cumulated vsize (Kb) 706952 [startup+440.038 s] Raw data (loadavg): 1.00 0.99 0.80 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 221004 0 3 0 42295 814 0 0 25 0 1 0 1851789180 732786688 178766 4294967295 134512640 135167914 3221224448 3220806656 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 178903 178766 162 162 0 178741 0 [pid=30219] vsize: 715612 Current children cumulated CPU time (s) 431.18 Current children cumulated vsize (Kb) 717740 [startup+450.039 s] Raw data (loadavg): 1.00 0.99 0.80 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 223121 0 3 0 43273 823 0 0 25 0 1 0 1851789180 741453824 180883 4294967295 134512640 135167914 3221224448 3220806592 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 181019 180883 162 162 0 180857 0 [pid=30219] vsize: 724076 Current children cumulated CPU time (s) 441.05 Current children cumulated vsize (Kb) 726204 [startup+460.039 s] Raw data (loadavg): 1.00 0.99 0.80 1/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 225265 0 3 0 44251 833 0 0 25 0 1 0 1851789180 750235648 183027 4294967295 134512640 135167914 3221224448 3220803964 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 183163 183027 162 162 0 183001 0 [pid=30219] vsize: 732652 Current children cumulated CPU time (s) 450.93 Current children cumulated vsize (Kb) 734780 [startup+470.04 s] Raw data (loadavg): 1.00 0.99 0.80 1/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 227596 0 3 0 45227 843 0 0 25 0 1 0 1851789180 759783424 185358 4294967295 134512640 135167914 3221224448 3220804924 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 185494 185358 162 162 0 185332 0 [pid=30219] vsize: 741976 Current children cumulated CPU time (s) 460.79 Current children cumulated vsize (Kb) 744104 [startup+480.041 s] Raw data (loadavg): 1.00 0.99 0.81 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 230398 0 3 0 46196 855 0 0 25 0 1 0 1851789180 771252224 188160 4294967295 134512640 135167914 3221224448 3220808732 134722229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 188294 188160 162 162 0 188132 0 [pid=30219] vsize: 753176 Current children cumulated CPU time (s) 470.6 Current children cumulated vsize (Kb) 755304 [startup+490.041 s] Raw data (loadavg): 1.00 0.99 0.81 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 232806 0 3 0 47171 866 0 0 25 0 1 0 1851789180 781107200 190568 4294967295 134512640 135167914 3221224448 3220806288 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 190700 190568 162 162 0 190538 0 [pid=30219] vsize: 762800 Current children cumulated CPU time (s) 480.46 Current children cumulated vsize (Kb) 764928 [startup+500.042 s] Raw data (loadavg): 1.00 0.99 0.81 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 234831 0 3 0 48152 873 0 0 25 0 1 0 1851789180 789397504 192593 4294967295 134512640 135167914 3221224448 3220806808 134845939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 192724 192593 162 162 0 192562 0 [pid=30219] vsize: 770896 Current children cumulated CPU time (s) 490.34 Current children cumulated vsize (Kb) 773024 [startup+510.042 s] Raw data (loadavg): 1.00 0.99 0.81 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 236883 0 3 0 49130 883 0 0 25 0 1 0 1851789180 797802496 194645 4294967295 134512640 135167914 3221224448 3220807168 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 194776 194645 162 162 0 194614 0 [pid=30219] vsize: 779104 Current children cumulated CPU time (s) 500.22 Current children cumulated vsize (Kb) 781232 [startup+520.042 s] Raw data (loadavg): 1.00 0.99 0.81 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 239349 0 3 0 50101 895 0 0 25 0 1 0 1851789180 807903232 197111 4294967295 134512640 135167914 3221224448 3220805592 134845877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 197242 197111 162 162 0 197080 0 [pid=30219] vsize: 788968 Current children cumulated CPU time (s) 510.05 Current children cumulated vsize (Kb) 791096 [startup+530.043 s] Raw data (loadavg): 1.00 0.99 0.81 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 242013 0 3 0 51075 905 0 0 25 0 1 0 1851789180 818806784 199775 4294967295 134512640 135167914 3221224448 3220813376 134843026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 199904 199775 162 162 0 199742 0 [pid=30219] vsize: 799616 Current children cumulated CPU time (s) 519.89 Current children cumulated vsize (Kb) 801744 [startup+540.044 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 244181 0 3 0 52051 914 0 0 25 0 1 0 1851789180 827682816 201943 4294967295 134512640 135167914 3221224448 3220809552 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 202071 201943 162 162 0 201909 0 [pid=30219] vsize: 808284 Current children cumulated CPU time (s) 529.74 Current children cumulated vsize (Kb) 810412 [startup+550.045 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 246127 0 3 0 53028 924 0 0 25 0 1 0 1851789180 835649536 203889 4294967295 134512640 135167914 3221224448 3220805888 134695806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 204016 203889 162 162 0 203854 0 [pid=30219] vsize: 816064 Current children cumulated CPU time (s) 539.61 Current children cumulated vsize (Kb) 818192 [startup+560.045 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 248152 0 3 0 54008 932 0 0 25 0 1 0 1851789180 843943936 205914 4294967295 134512640 135167914 3221224448 3220805788 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 206041 205914 162 162 0 205879 0 [pid=30219] vsize: 824164 Current children cumulated CPU time (s) 549.49 Current children cumulated vsize (Kb) 826292 [startup+570.046 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 250849 0 3 0 54980 945 0 0 25 0 1 0 1851789180 854990848 208611 4294967295 134512640 135167914 3221224448 3220804888 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 208738 208611 162 162 0 208576 0 [pid=30219] vsize: 834952 Current children cumulated CPU time (s) 559.34 Current children cumulated vsize (Kb) 837080 [startup+580.047 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 253228 0 3 0 55952 957 0 0 25 0 1 0 1851789180 864722944 210990 4294967295 134512640 135167914 3221224448 3220804192 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 211114 210990 162 162 0 210952 0 [pid=30219] vsize: 844456 Current children cumulated CPU time (s) 569.18 Current children cumulated vsize (Kb) 846584 [startup+590.048 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 255219 0 3 0 56928 967 0 0 25 0 1 0 1851789180 872873984 212976 4294967295 134512640 135167914 3221224448 3220809088 134619209 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 213104 212976 162 162 0 212942 0 [pid=30219] vsize: 852416 Current children cumulated CPU time (s) 579.04 Current children cumulated vsize (Kb) 854544 [startup+600.049 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 257104 0 5 0 57902 976 0 0 25 0 1 0 1851789180 880545792 214776 4294967295 134512640 135167914 3221224448 3220812912 134845913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 214977 214776 162 162 0 214815 0 [pid=30219] vsize: 859908 Current children cumulated CPU time (s) 588.87 Current children cumulated vsize (Kb) 862036 [startup+610.05 s] Raw data (loadavg): 1.00 0.99 0.82 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 259105 0 27 0 58861 986 0 0 25 0 1 0 1851789180 888401920 216597 4294967295 134512640 135167914 3221224448 3220804004 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 216895 216597 162 162 0 216733 0 [pid=30219] vsize: 867580 Current children cumulated CPU time (s) 598.56 Current children cumulated vsize (Kb) 869708 [startup+620.05 s] Raw data (loadavg): 1.00 0.99 0.83 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 261431 0 54 0 59809 996 0 0 25 0 1 0 1851789180 897343488 218830 4294967295 134512640 135167914 3221224448 3220804528 134623813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 219078 218830 162 162 0 218916 0 [pid=30219] vsize: 876312 Current children cumulated CPU time (s) 608.14 Current children cumulated vsize (Kb) 878440 [startup+630.051 s] Raw data (loadavg): 1.00 0.99 0.83 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 264336 0 71 0 60763 1008 0 0 25 0 1 0 1851789180 908484608 221665 4294967295 134512640 135167914 3221224448 3220818176 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30219/statm): 221798 221665 162 162 0 221636 0 [pid=30219] vsize: 887192 Current children cumulated CPU time (s) 617.8 Current children cumulated vsize (Kb) 889320 [startup+640.052 s] Raw data (loadavg): 1.00 0.99 0.83 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 266606 0 79 0 61733 1017 0 0 25 0 1 0 1851789180 917680128 223897 4294967295 134512640 135167914 3221224448 3220804812 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 224043 223897 162 162 0 223881 0 [pid=30219] vsize: 896172 Current children cumulated CPU time (s) 627.59 Current children cumulated vsize (Kb) 898300 [startup+650.053 s] Raw data (loadavg): 1.07 1.00 0.83 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 268435 0 103 0 62691 1025 0 0 25 0 1 0 1851789180 924905472 225538 4294967295 134512640 135167914 3221224448 3220813008 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 225807 225538 162 162 0 225645 0 [pid=30219] vsize: 903228 Current children cumulated CPU time (s) 637.25 Current children cumulated vsize (Kb) 905356 [startup+660.053 s] Raw data (loadavg): 1.06 1.00 0.83 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) R 30214 30214 19818 0 -1 0 270361 0 161 0 63615 1034 0 0 25 0 1 0 1851789180 931975168 227145 4294967295 134512640 135167914 3221224448 3220804724 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30219/statm): 227533 227147 162 162 0 227371 0 [pid=30219] vsize: 910132 Current children cumulated CPU time (s) 646.58 Current children cumulated vsize (Kb) 912260 [startup+670.053 s] Raw data (loadavg): 1.05 1.00 0.84 2/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 272342 0 192 0 64567 1044 0 0 25 0 1 0 1851789180 939249664 229046 4294967295 134512640 135167914 3221224448 3220806012 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 229309 229046 162 162 0 229147 0 [pid=30219] vsize: 917236 Current children cumulated CPU time (s) 656.2 Current children cumulated vsize (Kb) 919364 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+673.069 s] Raw data (loadavg): 1.05 1.00 0.84 1/57 30219 Raw data (/proc/30214/stat): 30214 (minisat+_script) S 30213 30214 19818 0 -1 0 314 531 0 2 0 1 6 2 17 0 1 0 1851789152 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30214/statm): 532 234 485 147 0 385 0 [pid=30214] vsize: 2128 Raw data (/proc/30219/stat): 30219 (minisat+_bignum) T 30214 30214 19818 0 -1 0 272962 0 199 0 64854 1047 0 0 25 0 1 0 1851789180 941543424 229660 4294967295 134512640 135167914 3221224448 3220805756 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30219/statm): 229869 229660 162 162 0 229707 0 [pid=30219] vsize: 919476 Current children cumulated CPU time (s) 659.1 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -30214 Sleeping 2 seconds One traced child (pid=30214) ended because it received signal 15 (SIGTERM) One traced child (pid=30219) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 673.501 CPU time (s): 659.449 CPU user time (s): 648.549 CPU system time (s): 10.8993 CPU usage (%): 97.9136 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !