Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-scsd1.opb |
MD5SUM | 18ccaf10caa576369b352d4f561a8c9e |
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 | 22800 |
Biggest coefficient in the objective function | 268435456000000000 |
Number of bits for the biggest coefficient in the objective function | 58 |
Sum of the numbers in the objective function | 188158757647584526336 |
Number of bits of the sum of numbers in the objective function | 68 |
Biggest number in a constraint | 268435456000000000 |
Number of bits of the biggest number in a constraint | 58 |
Biggest sum of numbers in a constraint | 188158757647584526336 |
Number of bits of the biggest sum of numbers | 68 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 22800 |
Total number of constraints | 77 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 77 |
Minimum length of a constraint | 600 |
Maximum length of a constraint | 1500 |
LAUNCH ON wulflinc21 THE 2005-09-18 20:31:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2807 boxname=wulflinc21 idbench=463 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 18ccaf10caa576369b352d4f561a8c9e /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb IDLAUNCH: 2807 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 889196 kB Buffers: 35252 kB Cached: 82568 kB SwapCached: 908 kB Active: 82308 kB Inactive: 38192 kB HighTotal: 131008 kB HighFree: 52248 kB LowTotal: 903652 kB LowFree: 836948 kB SwapTotal: 2097892 kB SwapFree: 2096472 kB Dirty: 52 kB Writeback: 0 kB Mapped: 5804 kB Slab: 19280 kB Committed_AS: 64368 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:40:14 (client local time) WITH STATUS 0 IN 490.66 SECONDS stats: 2807 7 490.66 0
c Parsing PB file... c PARSE ERROR! [line 764] 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/31957/stat): 31957 (minisat+_script) R 31956 31957 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1721426832 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31957/statm): 174 3 169 147 0 27 0 [pid=31957] 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=31958 New process pid=31959 New process pid=31960 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload One traced child (pid=31959) exited with status: 0 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=31960) exited with status: 0 One traced child (pid=31958) exited with status: 0 New process pid=31961 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb One traced child (pid=31961) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=31962 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb [startup+10.0028 s] Raw data (loadavg): 0.90 0.94 0.90 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 3112 0 0 0 959 15 0 0 25 0 1 0 1721426838 13500416 3056 4294967295 134512640 135167914 3221224448 3221221520 134845937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 3296 3056 162 162 0 3134 0 [pid=31962] vsize: 13184 Current children cumulated CPU time (s) 9.75 Current children cumulated vsize (Kb) 15312 [startup+20.0045 s] Raw data (loadavg): 0.92 0.94 0.90 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 8195 0 0 0 1912 37 0 0 25 0 1 0 1721426838 31383552 7427 4294967295 134512640 135167914 3221224448 3221061852 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31962/statm): 7662 7427 162 162 0 7500 0 [pid=31962] vsize: 30648 Current children cumulated CPU time (s) 19.5 Current children cumulated vsize (Kb) 32776 [startup+30.0052 s] Raw data (loadavg): 0.93 0.94 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 13227 0 0 0 2865 58 0 0 25 0 1 0 1721426838 49295360 11800 4294967295 134512640 135167914 3221224448 3221063712 134696045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 12035 11800 162 162 0 11873 0 [pid=31962] vsize: 48140 Current children cumulated CPU time (s) 29.24 Current children cumulated vsize (Kb) 50268 [startup+40.0059 s] Raw data (loadavg): 0.94 0.95 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 19463 0 0 0 3822 80 0 0 25 0 1 0 1721426838 69439488 16718 4294967295 134512640 135167914 3221224448 3221065104 134849179 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 16953 16718 162 162 0 16791 0 [pid=31962] vsize: 67812 Current children cumulated CPU time (s) 39.03 Current children cumulated vsize (Kb) 69940 [startup+50.0065 s] Raw data (loadavg): 0.95 0.95 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 23399 0 0 0 4782 96 0 0 25 0 1 0 1721426838 85561344 20654 4294967295 134512640 135167914 3221224448 3221063584 134843015 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 20889 20654 162 162 0 20727 0 [pid=31962] vsize: 83556 Current children cumulated CPU time (s) 48.79 Current children cumulated vsize (Kb) 85684 [startup+60.0062 s] Raw data (loadavg): 0.96 0.95 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 31978 0 0 0 5734 123 0 0 25 0 1 0 1721426838 109899776 26596 4294967295 134512640 135167914 3221224448 3221062640 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 26831 26596 162 162 0 26669 0 [pid=31962] vsize: 107324 Current children cumulated CPU time (s) 58.58 Current children cumulated vsize (Kb) 109452 [startup+70.0069 s] Raw data (loadavg): 0.96 0.95 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 35985 0 0 0 6686 143 0 0 25 0 1 0 1721426838 126312448 30603 4294967295 134512640 135167914 3221224448 3221061788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31962/statm): 30838 30603 162 162 0 30676 0 [pid=31962] vsize: 123352 Current children cumulated CPU time (s) 68.3 Current children cumulated vsize (Kb) 125480 [startup+80.0076 s] Raw data (loadavg): 0.97 0.95 0.91 1/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 39967 0 0 0 7644 159 0 0 25 0 1 0 1721426838 142622720 34585 4294967295 134512640 135167914 3221224448 3221061564 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31962/statm): 34820 34585 162 162 0 34658 0 [pid=31962] vsize: 139280 Current children cumulated CPU time (s) 78.04 Current children cumulated vsize (Kb) 141408 [startup+90.0083 s] Raw data (loadavg): 0.97 0.95 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 44093 0 0 0 8597 180 0 0 25 0 1 0 1721426838 159522816 38711 4294967295 134512640 135167914 3221224448 3221062860 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 38946 38711 162 162 0 38784 0 [pid=31962] vsize: 155784 Current children cumulated CPU time (s) 87.78 Current children cumulated vsize (Kb) 157912 [startup+100.009 s] Raw data (loadavg): 0.98 0.95 0.91 1/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 56908 0 0 0 9547 213 0 0 25 0 1 0 1721426838 190414848 46253 4294967295 134512640 135167914 3221224448 3221062460 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31962/statm): 46488 46253 162 162 0 46326 0 [pid=31962] vsize: 185952 Current children cumulated CPU time (s) 97.61 Current children cumulated vsize (Kb) 188080 [startup+110.01 s] Raw data (loadavg): 0.98 0.95 0.91 1/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 61065 0 0 0 10503 230 0 0 25 0 1 0 1721426838 207441920 50410 4294967295 134512640 135167914 3221224448 3221063196 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31962/statm): 50645 50410 162 162 0 50483 0 [pid=31962] vsize: 202580 Current children cumulated CPU time (s) 107.34 Current children cumulated vsize (Kb) 204708 [startup+120.011 s] Raw data (loadavg): 0.98 0.95 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 65039 0 0 0 11458 248 0 0 25 0 1 0 1721426838 223719424 54384 4294967295 134512640 135167914 3221224448 3221061968 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 54619 54384 162 162 0 54457 0 [pid=31962] vsize: 218476 Current children cumulated CPU time (s) 117.07 Current children cumulated vsize (Kb) 220604 [startup+130.012 s] Raw data (loadavg): 0.98 0.95 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 68972 0 0 0 12417 265 0 0 25 0 1 0 1721426838 239828992 58317 4294967295 134512640 135167914 3221224448 3221063536 134694351 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 58552 58317 162 162 0 58390 0 [pid=31962] vsize: 234208 Current children cumulated CPU time (s) 126.83 Current children cumulated vsize (Kb) 236336 [startup+140.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 72988 0 0 0 13374 283 0 0 25 0 1 0 1721426838 256282624 62333 4294967295 134512640 135167914 3221224448 3221064080 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31962/statm): 62569 62333 162 162 0 62407 0 [pid=31962] vsize: 250276 Current children cumulated CPU time (s) 136.58 Current children cumulated vsize (Kb) 252404 [startup+150.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 77114 0 0 0 14330 302 0 0 25 0 1 0 1721426838 273182720 66459 4294967295 134512640 135167914 3221224448 3221065600 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 66695 66459 162 162 0 66533 0 [pid=31962] vsize: 266780 Current children cumulated CPU time (s) 146.33 Current children cumulated vsize (Kb) 268908 [startup+160.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 81062 0 0 0 15286 320 0 0 25 0 1 0 1721426838 289349632 70407 4294967295 134512640 135167914 3221224448 3221062356 134697279 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 70642 70407 162 162 0 70480 0 [pid=31962] vsize: 282568 Current children cumulated CPU time (s) 156.07 Current children cumulated vsize (Kb) 284696 [startup+170.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 85044 0 0 0 16243 338 0 0 25 0 1 0 1721426838 305659904 74389 4294967295 134512640 135167914 3221224448 3221063956 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31962/statm): 74624 74389 162 162 0 74462 0 [pid=31962] vsize: 298496 Current children cumulated CPU time (s) 165.82 Current children cumulated vsize (Kb) 300624 [startup+180.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 109232 0 0 0 17161 400 0 0 25 0 1 0 1721426838 404733952 98577 4294967295 134512640 135167914 3221224448 3221063252 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 98812 98577 162 162 0 98650 0 [pid=31962] vsize: 395248 Current children cumulated CPU time (s) 175.62 Current children cumulated vsize (Kb) 397376 [startup+190.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 110893 0 0 0 18141 409 0 0 25 0 1 0 1721426838 368340992 89692 4294967295 134512640 135167914 3221224448 3221062496 134722532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31962/statm): 89927 89692 162 162 0 89765 0 [pid=31962] vsize: 359708 Current children cumulated CPU time (s) 185.51 Current children cumulated vsize (Kb) 361836 [startup+200.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 115015 0 0 0 19099 427 0 0 25 0 1 0 1721426838 385224704 93814 4294967295 134512640 135167914 3221224448 3221062820 134845880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 94049 93814 162 162 0 93887 0 [pid=31962] vsize: 376196 Current children cumulated CPU time (s) 195.27 Current children cumulated vsize (Kb) 378324 [startup+210.015 s] Raw data (loadavg): 0.99 0.96 0.91 1/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 119309 0 0 0 20050 449 0 0 25 0 1 0 1721426838 402812928 98108 4294967295 134512640 135167914 3221224448 3221062684 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/31962/statm): 98343 98108 162 162 0 98181 0 [pid=31962] vsize: 393372 Current children cumulated CPU time (s) 205 Current children cumulated vsize (Kb) 395500 [startup+220.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 123571 0 0 0 21004 465 0 0 25 0 1 0 1721426838 420270080 102370 4294967295 134512640 135167914 3221224448 3221063852 134844675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 102605 102370 162 162 0 102443 0 [pid=31962] vsize: 410420 Current children cumulated CPU time (s) 214.7 Current children cumulated vsize (Kb) 412548 [startup+230.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 127748 0 0 0 21959 483 0 0 25 0 1 0 1721426838 437379072 106547 4294967295 134512640 135167914 3221224448 3221061788 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 106782 106547 162 162 0 106620 0 [pid=31962] vsize: 427128 Current children cumulated CPU time (s) 224.43 Current children cumulated vsize (Kb) 429256 [startup+240.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 131798 0 0 0 22914 502 0 0 25 0 1 0 1721426838 453967872 110597 4294967295 134512640 135167914 3221224448 3221062752 134694419 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 110832 110597 162 162 0 110670 0 [pid=31962] vsize: 443328 Current children cumulated CPU time (s) 234.17 Current children cumulated vsize (Kb) 445456 [startup+250.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 135842 0 0 0 23871 520 0 0 25 0 1 0 1721426838 470532096 114641 4294967295 134512640 135167914 3221224448 3221062768 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 114876 114641 162 162 0 114714 0 [pid=31962] vsize: 459504 Current children cumulated CPU time (s) 243.92 Current children cumulated vsize (Kb) 461632 [startup+260.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 139927 0 0 0 24826 540 0 0 25 0 1 0 1721426838 487264256 118726 4294967295 134512640 135167914 3221224448 3221061776 134621149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31962/statm): 118961 118726 162 162 0 118799 0 [pid=31962] vsize: 475844 Current children cumulated CPU time (s) 253.67 Current children cumulated vsize (Kb) 477972 [startup+270.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 143791 0 0 0 25785 556 0 0 25 0 1 0 1721426838 503091200 122590 4294967295 134512640 135167914 3221224448 3221062620 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 122825 122590 162 162 0 122663 0 [pid=31962] vsize: 491300 Current children cumulated CPU time (s) 263.42 Current children cumulated vsize (Kb) 493428 [startup+280.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 147743 0 0 0 26742 573 0 0 25 0 1 0 1721426838 519286784 126542 4294967295 134512640 135167914 3221224448 3221063312 134849096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 126779 126542 162 162 0 126617 0 [pid=31962] vsize: 507116 Current children cumulated CPU time (s) 273.16 Current children cumulated vsize (Kb) 509244 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 151697 0 0 0 27699 591 0 0 25 0 1 0 1721426838 535482368 130496 4294967295 134512640 135167914 3221224448 3221063936 134722527 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31962/statm): 130733 130496 162 162 0 130571 0 [pid=31962] vsize: 522932 Current children cumulated CPU time (s) 282.91 Current children cumulated vsize (Kb) 525060 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 155697 0 0 0 28656 609 0 0 25 0 1 0 1721426838 551866368 134496 4294967295 134512640 135167914 3221224448 3221063344 134619572 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 134733 134496 162 162 0 134571 0 [pid=31962] vsize: 538932 Current children cumulated CPU time (s) 292.66 Current children cumulated vsize (Kb) 541060 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 159505 0 0 0 29614 628 0 0 25 0 1 0 1721426838 567463936 138304 4294967295 134512640 135167914 3221224448 3221065344 134621119 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 138541 138304 162 162 0 138379 0 [pid=31962] vsize: 554164 Current children cumulated CPU time (s) 302.43 Current children cumulated vsize (Kb) 556292 [startup+320.023 s] Raw data (loadavg): 0.99 0.97 0.91 1/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 163311 0 0 0 30572 646 0 0 25 0 1 0 1721426838 583053312 142110 4294967295 134512640 135167914 3221224448 3221062300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31962/statm): 142347 142110 162 162 0 142185 0 [pid=31962] vsize: 569388 Current children cumulated CPU time (s) 312.19 Current children cumulated vsize (Kb) 571516 [startup+330.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 167164 0 0 0 31530 663 0 0 25 0 1 0 1721426838 598835200 145963 4294967295 134512640 135167914 3221224448 3221062912 134844866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 146200 145963 162 162 0 146038 0 [pid=31962] vsize: 584800 Current children cumulated CPU time (s) 321.94 Current children cumulated vsize (Kb) 586928 [startup+340.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 171017 0 0 0 32490 680 0 0 25 0 1 0 1721426838 614617088 149816 4294967295 134512640 135167914 3221224448 3221062784 134624387 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 150053 149816 162 162 0 149891 0 [pid=31962] vsize: 600212 Current children cumulated CPU time (s) 331.71 Current children cumulated vsize (Kb) 602340 [startup+350.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 215010 0 0 0 33376 783 0 0 25 0 1 0 1721426838 794808320 193809 4294967295 134512640 135167914 3221224448 3221063276 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 194045 193809 162 162 0 193883 0 [pid=31962] vsize: 776180 Current children cumulated CPU time (s) 341.6 Current children cumulated vsize (Kb) 778308 [startup+360.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 215010 0 0 0 34376 783 0 0 25 0 1 0 1721426838 794808320 193809 4294967295 134512640 135167914 3221224448 3221063328 134625428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 194045 193809 162 162 0 193883 0 [pid=31962] vsize: 776180 Current children cumulated CPU time (s) 351.6 Current children cumulated vsize (Kb) 778308 [startup+370.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 218424 0 0 0 35335 803 0 0 25 0 1 0 1721426838 722407424 176132 4294967295 134512640 135167914 3221224448 3221061696 134854320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 176369 176132 162 162 0 176207 0 [pid=31962] vsize: 705476 Current children cumulated CPU time (s) 361.39 Current children cumulated vsize (Kb) 707604 [startup+380.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 222584 0 0 0 36286 822 0 0 25 0 1 0 1721426838 739442688 180292 4294967295 134512640 135167914 3221224448 3221063456 134623781 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 180528 180292 162 162 0 180366 0 [pid=31962] vsize: 722112 Current children cumulated CPU time (s) 371.09 Current children cumulated vsize (Kb) 724240 [startup+390.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 226823 0 0 0 37240 839 0 0 25 0 1 0 1721426838 756805632 184531 4294967295 134512640 135167914 3221224448 3221063304 134722657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 184767 184531 162 162 0 184605 0 [pid=31962] vsize: 739068 Current children cumulated CPU time (s) 380.8 Current children cumulated vsize (Kb) 741196 [startup+400.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 230981 0 0 0 38196 857 0 0 25 0 1 0 1721426838 773836800 188689 4294967295 134512640 135167914 3221224448 3221063612 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31962/statm): 188925 188689 162 162 0 188763 0 [pid=31962] vsize: 755700 Current children cumulated CPU time (s) 390.54 Current children cumulated vsize (Kb) 757828 [startup+410.028 s] Raw data (loadavg): 1.07 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 235103 0 0 0 39150 875 0 0 24 0 1 0 1721426838 790720512 192811 4294967295 134512640 135167914 3221224448 3221064560 134849179 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31962/statm): 193047 192811 162 162 0 192885 0 [pid=31962] vsize: 772188 Current children cumulated CPU time (s) 400.26 Current children cumulated vsize (Kb) 774316 [startup+420.029 s] Raw data (loadavg): 1.06 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 239122 0 0 0 40106 896 0 0 25 0 1 0 1721426838 807182336 196830 4294967295 134512640 135167914 3221224448 3221063744 134849179 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 197066 196830 162 162 0 196904 0 [pid=31962] vsize: 788264 Current children cumulated CPU time (s) 410.03 Current children cumulated vsize (Kb) 790392 [startup+430.029 s] Raw data (loadavg): 1.05 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 243114 0 0 0 41058 915 0 0 25 0 1 0 1721426838 823533568 200822 4294967295 134512640 135167914 3221224448 3221062576 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 201058 200822 162 162 0 200896 0 [pid=31962] vsize: 804232 Current children cumulated CPU time (s) 419.74 Current children cumulated vsize (Kb) 806360 [startup+440.03 s] Raw data (loadavg): 1.04 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 247112 0 0 0 42018 933 0 0 25 0 1 0 1721426838 839909376 204820 4294967295 134512640 135167914 3221224448 3221061776 134618969 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31962/statm): 205056 204820 162 162 0 204894 0 [pid=31962] vsize: 820224 Current children cumulated CPU time (s) 429.52 Current children cumulated vsize (Kb) 822352 [startup+450.031 s] Raw data (loadavg): 1.04 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 251112 0 0 0 42969 953 0 0 25 0 1 0 1721426838 856293376 208820 4294967295 134512640 135167914 3221224448 3221062844 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 209056 208820 162 162 0 208894 0 [pid=31962] vsize: 836224 Current children cumulated CPU time (s) 439.23 Current children cumulated vsize (Kb) 838352 [startup+460.031 s] Raw data (loadavg): 1.03 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 255062 0 0 0 43927 970 0 0 25 0 1 0 1721426838 872472576 212770 4294967295 134512640 135167914 3221224448 3221062384 134522460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 213006 212770 162 162 0 212844 0 [pid=31962] vsize: 852024 Current children cumulated CPU time (s) 448.98 Current children cumulated vsize (Kb) 854152 [startup+470.032 s] Raw data (loadavg): 1.03 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 259023 0 0 0 44882 987 0 0 25 0 1 0 1721426838 888696832 216731 4294967295 134512640 135167914 3221224448 3221062868 134619947 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 216967 216731 162 162 0 216805 0 [pid=31962] vsize: 867868 Current children cumulated CPU time (s) 458.7 Current children cumulated vsize (Kb) 869996 [startup+480.033 s] Raw data (loadavg): 1.02 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 263010 0 0 0 45843 1003 0 0 25 0 1 0 1721426838 905027584 220718 4294967295 134512640 135167914 3221224448 3221063360 134845396 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 220954 220718 162 162 0 220792 0 [pid=31962] vsize: 883816 Current children cumulated CPU time (s) 468.47 Current children cumulated vsize (Kb) 885944 [startup+490.034 s] Raw data (loadavg): 1.02 0.99 0.91 2/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 267052 0 46 0 46756 1024 0 0 25 0 1 0 1721426838 920588288 224316 4294967295 134512640 135167914 3221224448 3221062992 134693558 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31962/statm): 224753 224316 162 162 0 224591 0 [pid=31962] vsize: 899012 Current children cumulated CPU time (s) 477.81 Current children cumulated vsize (Kb) 901140 [startup+500.035 s] Raw data (loadavg): 1.01 0.99 0.91 1/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 271072 0 50 0 47702 1048 0 0 25 0 1 0 1721426838 936988672 227755 4294967295 134512640 135167914 3221224448 3221063196 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/31962/statm): 228757 227755 162 162 0 228595 0 [pid=31962] vsize: 915028 Current children cumulated CPU time (s) 487.51 Current children cumulated vsize (Kb) 917156 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+502.891 s] Raw data (loadavg): 1.01 0.99 0.91 1/58 31962 Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31957/statm): 532 234 485 147 0 385 0 [pid=31957] vsize: 2128 Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 272192 0 54 0 47969 1053 0 0 25 0 1 0 1721426838 941543424 228465 4294967295 134512640 135167914 3221224448 3221062396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/31962/statm): 229869 228465 162 162 0 229707 0 [pid=31962] vsize: 919476 Current children cumulated CPU time (s) 490.23 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -31957 Sleeping 2 seconds One traced child (pid=31957) ended because it received signal 15 (SIGTERM) One traced child (pid=31962) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 503.319 CPU time (s): 490.66 CPU user time (s): 479.699 CPU system time (s): 10.9613 CPU usage (%): 97.4849 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !