Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-net12.opb |
MD5SUM | 8fd050825d75dbe16d9da083f4b2fd63 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 8257573732279 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 478 |
Biggest coefficient in the objective function | 536870912000000 |
Number of bits for the biggest coefficient in the objective function | 49 |
Sum of the numbers in the objective function | 1073761158741413 |
Number of bits of the sum of numbers in the objective function | 50 |
Biggest number in a constraint | 71583145981965762560 |
Number of bits of the biggest number in a constraint | 66 |
Biggest sum of numbers in a constraint | 303620978593259257856 |
Number of bits of the biggest sum of numbers | 69 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1269.78 |
Number of variables | 780 |
Total number of constraints | 707 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 338 |
Number of constraints which are nor clauses,nor cardinality constraints | 369 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 101 |
LAUNCH ON wulflinc25 THE 2005-09-20 02:08:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3108 boxname=wulflinc25 idbench=764 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8fd050825d75dbe16d9da083f4b2fd63 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb IDLAUNCH: 3108 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 924752 kB Buffers: 2216 kB Cached: 79756 kB SwapCached: 852 kB Active: 20388 kB Inactive: 64120 kB HighTotal: 131008 kB HighFree: 47908 kB LowTotal: 903652 kB LowFree: 876844 kB SwapTotal: 2097892 kB SwapFree: 2096524 kB Dirty: 36 kB Writeback: 0 kB Mapped: 5720 kB Slab: 19532 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:15:05 (client local time) WITH STATUS 0 IN 400.237 SECONDS stats: 3108 7 400.237 0
c Parsing PB file... c PARSE ERROR! [line 326] 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/26429/stat): 26429 (minisat+_script) R 26428 26429 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854843804 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/26429/statm): 174 3 169 147 0 27 0 [pid=26429] 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=26430 New process pid=26431 New process pid=26432 execve syscall for /bin/sed executable One traced child (pid=26431) 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=26432) exited with status: 0 One traced child (pid=26430) exited with status: 0 New process pid=26433 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb One traced child (pid=26433) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=26434 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-net12.opb [startup+10.0031 s] Raw data (loadavg): 1.06 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 5168 0 0 0 945 23 0 0 25 0 1 0 1854843811 19046400 4534 4294967295 134512640 135167914 3221224448 3221201516 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 4650 4534 162 162 0 4488 0 [pid=26434] vsize: 18600 Current children cumulated CPU time (s) 9.7 Current children cumulated vsize (Kb) 20728 [startup+20.0047 s] Raw data (loadavg): 1.05 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 13911 0 0 0 1878 58 0 0 25 0 1 0 1854843811 52158464 12618 4294967295 134512640 135167914 3221224448 3221200640 134625414 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 12734 12618 162 162 0 12572 0 [pid=26434] vsize: 50936 Current children cumulated CPU time (s) 19.38 Current children cumulated vsize (Kb) 53064 [startup+30.0053 s] Raw data (loadavg): 1.04 0.99 0.94 1/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 18434 0 0 0 2827 79 0 0 25 0 1 0 1854843811 65286144 15823 4294967295 134512640 135167914 3221224448 3221201372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 15939 15823 162 162 0 15777 0 [pid=26434] vsize: 63756 Current children cumulated CPU time (s) 29.08 Current children cumulated vsize (Kb) 65884 [startup+40.0049 s] Raw data (loadavg): 1.03 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 27650 0 0 0 3777 107 0 0 25 0 1 0 1854843811 92233728 22402 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 22518 22402 162 162 0 22356 0 [pid=26434] vsize: 90072 Current children cumulated CPU time (s) 38.86 Current children cumulated vsize (Kb) 92200 [startup+50.0055 s] Raw data (loadavg): 1.03 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 32403 0 0 0 4723 128 0 0 25 0 1 0 1854843811 111702016 27155 4294967295 134512640 135167914 3221224448 3221202844 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 27271 27155 162 162 0 27109 0 [pid=26434] vsize: 109084 Current children cumulated CPU time (s) 48.53 Current children cumulated vsize (Kb) 111212 [startup+60.0061 s] Raw data (loadavg): 1.02 0.99 0.94 1/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 37240 0 0 0 5674 147 0 0 25 0 1 0 1854843811 131514368 31992 4294967295 134512640 135167914 3221224448 3221201148 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 32108 31992 162 162 0 31946 0 [pid=26434] vsize: 128432 Current children cumulated CPU time (s) 58.23 Current children cumulated vsize (Kb) 130560 [startup+70.0067 s] Raw data (loadavg): 1.02 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 42090 0 0 0 6620 169 0 0 25 0 1 0 1854843811 151379968 36842 4294967295 134512640 135167914 3221224448 3221201224 134693631 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 36958 36842 162 162 0 36796 0 [pid=26434] vsize: 147832 Current children cumulated CPU time (s) 67.91 Current children cumulated vsize (Kb) 149960 [startup+80.0073 s] Raw data (loadavg): 1.02 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 55561 0 0 0 7561 208 0 0 25 0 1 0 1854843811 184958976 45040 4294967295 134512640 135167914 3221224448 3221201888 134624387 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 45156 45040 162 162 0 44994 0 [pid=26434] vsize: 180624 Current children cumulated CPU time (s) 77.71 Current children cumulated vsize (Kb) 182752 [startup+90.0069 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 60658 0 0 0 8503 234 0 0 25 0 1 0 1854843811 205836288 50137 4294967295 134512640 135167914 3221224448 3221200848 134849096 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 50253 50137 162 162 0 50091 0 [pid=26434] vsize: 201012 Current children cumulated CPU time (s) 87.39 Current children cumulated vsize (Kb) 203140 [startup+100.007 s] Raw data (loadavg): 1.01 0.99 0.94 1/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 65525 0 0 0 9451 254 0 0 24 0 1 0 1854843811 225771520 55004 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 55120 55004 162 162 0 54958 0 [pid=26434] vsize: 220480 Current children cumulated CPU time (s) 97.07 Current children cumulated vsize (Kb) 222608 [startup+110.008 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 70323 0 0 0 10397 278 0 0 25 0 1 0 1854843811 245424128 59802 4294967295 134512640 135167914 3221224448 3221201408 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 59918 59802 162 162 0 59756 0 [pid=26434] vsize: 239672 Current children cumulated CPU time (s) 106.77 Current children cumulated vsize (Kb) 241800 [startup+120.01 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 75143 0 0 0 11346 301 0 0 25 0 1 0 1854843811 265166848 64622 4294967295 134512640 135167914 3221224448 3221200764 134722576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 64738 64622 162 162 0 64576 0 [pid=26434] vsize: 258952 Current children cumulated CPU time (s) 116.49 Current children cumulated vsize (Kb) 261080 [startup+130.01 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 79948 0 0 0 12294 323 0 0 25 0 1 0 1854843811 284848128 69427 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 69543 69427 162 162 0 69381 0 [pid=26434] vsize: 278172 Current children cumulated CPU time (s) 126.19 Current children cumulated vsize (Kb) 280300 [startup+140.01 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 84843 0 0 0 13239 344 0 0 25 0 1 0 1854843811 304898048 74322 4294967295 134512640 135167914 3221224448 3221201440 134624226 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 74438 74322 162 162 0 74276 0 [pid=26434] vsize: 297752 Current children cumulated CPU time (s) 135.85 Current children cumulated vsize (Kb) 299880 [startup+150.011 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 106786 0 0 0 14182 397 0 0 25 0 1 0 1854843811 351580160 85719 4294967295 134512640 135167914 3221224448 3221202112 134624153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 85835 85719 162 162 0 85673 0 [pid=26434] vsize: 343340 Current children cumulated CPU time (s) 145.81 Current children cumulated vsize (Kb) 345468 [startup+160.011 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 111934 0 0 0 15125 420 0 0 25 0 1 0 1854843811 372666368 90867 4294967295 134512640 135167914 3221224448 3221201520 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 90983 90867 162 162 0 90821 0 [pid=26434] vsize: 363932 Current children cumulated CPU time (s) 155.47 Current children cumulated vsize (Kb) 366060 [startup+170.012 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 116934 0 0 0 16071 443 0 0 25 0 1 0 1854843811 393146368 95867 4294967295 134512640 135167914 3221224448 3221200384 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 95983 95867 162 162 0 95821 0 [pid=26434] vsize: 383932 Current children cumulated CPU time (s) 165.16 Current children cumulated vsize (Kb) 386060 [startup+180.012 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 121955 0 0 0 17018 467 0 0 25 0 1 0 1854843811 413712384 100888 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 101004 100888 162 162 0 100842 0 [pid=26434] vsize: 404016 Current children cumulated CPU time (s) 174.87 Current children cumulated vsize (Kb) 406144 [startup+190.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 126980 0 0 0 17957 491 0 0 25 0 1 0 1854843811 434294784 105913 4294967295 134512640 135167914 3221224448 3221200572 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 106029 105913 162 162 0 105867 0 [pid=26434] vsize: 424116 Current children cumulated CPU time (s) 184.5 Current children cumulated vsize (Kb) 426244 [startup+200.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 131996 0 0 0 18908 512 0 0 25 0 1 0 1854843811 454840320 110929 4294967295 134512640 135167914 3221224448 3221200928 134722539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 111045 110929 162 162 0 110883 0 [pid=26434] vsize: 444180 Current children cumulated CPU time (s) 194.22 Current children cumulated vsize (Kb) 446308 [startup+210.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 136904 0 0 0 19849 535 0 0 25 0 1 0 1854843811 474943488 115837 4294967295 134512640 135167914 3221224448 3221200552 134693665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 115953 115837 162 162 0 115791 0 [pid=26434] vsize: 463812 Current children cumulated CPU time (s) 203.86 Current children cumulated vsize (Kb) 465940 [startup+220.016 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 141787 0 0 0 20796 557 0 0 25 0 1 0 1854843811 494944256 120720 4294967295 134512640 135167914 3221224448 3221200480 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 120836 120720 162 162 0 120674 0 [pid=26434] vsize: 483344 Current children cumulated CPU time (s) 213.55 Current children cumulated vsize (Kb) 485472 [startup+230.016 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 146498 0 0 0 21741 579 0 0 25 0 1 0 1854843811 514240512 125431 4294967295 134512640 135167914 3221224448 3221200840 134849057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 125547 125431 162 162 0 125385 0 [pid=26434] vsize: 502188 Current children cumulated CPU time (s) 223.22 Current children cumulated vsize (Kb) 504316 [startup+240.017 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 151474 0 0 0 22689 602 0 0 25 0 1 0 1854843811 534622208 130407 4294967295 134512640 135167914 3221224448 3221200876 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 130523 130407 162 162 0 130361 0 [pid=26434] vsize: 522092 Current children cumulated CPU time (s) 232.93 Current children cumulated vsize (Kb) 524220 [startup+250.018 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 156308 0 0 0 23636 626 0 0 25 0 1 0 1854843811 554422272 135241 4294967295 134512640 135167914 3221224448 3221201884 134693552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 135357 135241 162 162 0 135195 0 [pid=26434] vsize: 541428 Current children cumulated CPU time (s) 242.64 Current children cumulated vsize (Kb) 543556 [startup+260.018 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 161021 0 0 0 24584 647 0 0 25 0 1 0 1854843811 573726720 139954 4294967295 134512640 135167914 3221224448 3221201940 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 140070 139954 162 162 0 139908 0 [pid=26434] vsize: 560280 Current children cumulated CPU time (s) 252.33 Current children cumulated vsize (Kb) 562408 [startup+270.019 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 165709 0 0 0 25530 669 0 0 25 0 1 0 1854843811 592928768 144642 4294967295 134512640 135167914 3221224448 3221202224 134845901 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 144758 144642 162 162 0 144596 0 [pid=26434] vsize: 579032 Current children cumulated CPU time (s) 262.01 Current children cumulated vsize (Kb) 581160 [startup+280.019 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 192739 0 0 0 26429 742 0 0 25 0 1 0 1854843811 783515648 171672 4294967295 134512640 135167914 3221224448 3221201536 134625368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 191288 171679 162 162 0 191126 0 [pid=26434] vsize: 765152 Current children cumulated CPU time (s) 271.73 Current children cumulated vsize (Kb) 767280 [startup+290.02 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 212239 0 0 0 27384 787 0 0 25 0 1 0 1854843811 783515648 191172 4294967295 134512640 135167914 3221224448 3221201488 134694435 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 191288 191172 162 162 0 191126 0 [pid=26434] vsize: 765152 Current children cumulated CPU time (s) 281.73 Current children cumulated vsize (Kb) 767280 [startup+300.021 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 214229 0 0 0 28358 799 0 0 25 0 1 0 1854843811 705277952 172071 4294967295 134512640 135167914 3221224448 3221200620 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 172187 172071 162 162 0 172025 0 [pid=26434] vsize: 688748 Current children cumulated CPU time (s) 291.59 Current children cumulated vsize (Kb) 690876 [startup+310.021 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 219171 0 0 0 29304 819 0 0 25 0 1 0 1854843811 725520384 177013 4294967295 134512640 135167914 3221224448 3221201200 134624975 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 177129 177013 162 162 0 176967 0 [pid=26434] vsize: 708516 Current children cumulated CPU time (s) 301.25 Current children cumulated vsize (Kb) 710644 [startup+320.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 224344 0 0 0 30244 845 0 0 25 0 1 0 1854843811 746708992 182186 4294967295 134512640 135167914 3221224448 3221201728 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 182302 182186 162 162 0 182140 0 [pid=26434] vsize: 729208 Current children cumulated CPU time (s) 310.91 Current children cumulated vsize (Kb) 731336 [startup+330.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 229559 0 0 0 31188 869 0 0 25 0 1 0 1854843811 768069632 187401 4294967295 134512640 135167914 3221224448 3221201468 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 187517 187401 162 162 0 187355 0 [pid=26434] vsize: 750068 Current children cumulated CPU time (s) 320.59 Current children cumulated vsize (Kb) 752196 [startup+340.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 234661 0 0 0 32130 895 0 0 25 0 1 0 1854843811 788967424 192503 4294967295 134512640 135167914 3221224448 3221201440 134622385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 192619 192503 162 162 0 192457 0 [pid=26434] vsize: 770476 Current children cumulated CPU time (s) 330.27 Current children cumulated vsize (Kb) 772604 [startup+350.023 s] Raw data (loadavg): 1.00 0.99 0.94 1/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 239857 0 0 0 33079 914 0 0 25 0 1 0 1854843811 810250240 197699 4294967295 134512640 135167914 3221224448 3221200700 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 197815 197699 162 162 0 197653 0 [pid=26434] vsize: 791260 Current children cumulated CPU time (s) 339.95 Current children cumulated vsize (Kb) 793388 [startup+360.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 245011 0 0 0 34022 939 0 0 25 0 1 0 1854843811 831361024 202853 4294967295 134512640 135167914 3221224448 3221201264 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 202969 202853 162 162 0 202807 0 [pid=26434] vsize: 811876 Current children cumulated CPU time (s) 349.63 Current children cumulated vsize (Kb) 814004 [startup+370.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 250181 0 0 0 34959 966 0 0 25 0 1 0 1854843811 852537344 208023 4294967295 134512640 135167914 3221224448 3221201408 134843068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 208139 208023 162 162 0 207977 0 [pid=26434] vsize: 832556 Current children cumulated CPU time (s) 359.27 Current children cumulated vsize (Kb) 834684 [startup+380.024 s] Raw data (loadavg): 1.07 1.00 0.95 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 255425 0 0 0 35901 989 0 0 25 0 1 0 1854843811 874016768 213267 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26434/statm): 213383 213267 162 162 0 213221 0 [pid=26434] vsize: 853532 Current children cumulated CPU time (s) 368.92 Current children cumulated vsize (Kb) 855660 [startup+390.024 s] Raw data (loadavg): 1.06 1.00 0.95 1/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 260603 0 0 0 36841 1015 0 0 25 0 1 0 1854843811 895229952 218445 4294967295 134512640 135167914 3221224448 3221200476 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26434/statm): 218562 218445 162 162 0 218400 0 [pid=26434] vsize: 874248 Current children cumulated CPU time (s) 378.58 Current children cumulated vsize (Kb) 876376 [startup+400.025 s] Raw data (loadavg): 1.05 1.00 0.95 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 265767 0 0 0 37782 1038 0 0 25 0 1 0 1854843811 916377600 223609 4294967295 134512640 135167914 3221224448 3221200640 134621159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26434/statm): 223725 223609 162 162 0 223563 0 [pid=26434] vsize: 894900 Current children cumulated CPU time (s) 388.22 Current children cumulated vsize (Kb) 897028 [startup+410.025 s] Raw data (loadavg): 1.04 1.00 0.95 2/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) R 26429 26429 4419 0 -1 0 270883 0 0 0 38721 1064 0 0 25 0 1 0 1854843811 937332736 228725 4294967295 134512640 135167914 3221224448 3221200928 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26434/statm): 228841 228725 162 162 0 228679 0 [pid=26434] vsize: 915364 Current children cumulated CPU time (s) 397.87 Current children cumulated vsize (Kb) 917492 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+412.057 s] Raw data (loadavg): 1.04 1.00 0.95 1/57 26434 Raw data (/proc/26429/stat): 26429 (minisat+_script) S 26428 26429 4419 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854843804 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26429/statm): 532 234 485 147 0 385 0 [pid=26429] vsize: 2128 Raw data (/proc/26434/stat): 26434 (minisat+_bignum) T 26429 26429 4419 0 -1 0 271910 0 0 0 38911 1069 0 0 25 0 1 0 1854843811 941543424 229752 4294967295 134512640 135167914 3221224448 3221201788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26434/statm): 229869 229752 162 162 0 229707 0 [pid=26434] vsize: 919476 Current children cumulated CPU time (s) 399.82 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -26429 Sleeping 2 seconds One traced child (pid=26429) ended because it received signal 15 (SIGTERM) One traced child (pid=26434) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 412.487 CPU time (s): 400.237 CPU user time (s): 389.119 CPU system time (s): 11.1183 CPU usage (%): 97.0303 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !