Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-scsd8.opb |
MD5SUM | 63dde7c8c3b02bd89e3e065c5bd58b69 |
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 | 82500 |
Biggest coefficient in the objective function | 221357547985043456 |
Number of bits for the biggest coefficient in the objective function | 58 |
Sum of the numbers in the objective function | 595796164546237562880 |
Number of bits of the sum of numbers in the objective function | 70 |
Biggest number in a constraint | 221357547985043456 |
Number of bits of the biggest number in a constraint | 58 |
Biggest sum of numbers in a constraint | 595796164546237562880 |
Number of bits of the biggest sum of numbers | 70 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 82500 |
Total number of constraints | 397 |
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 | 397 |
Minimum length of a constraint | 300 |
Maximum length of a constraint | 720 |
LAUNCH ON wulflinc18 THE 2005-09-18 20:32:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2809 boxname=wulflinc18 idbench=465 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 63dde7c8c3b02bd89e3e065c5bd58b69 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb IDLAUNCH: 2809 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 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: 902156 kB Buffers: 35432 kB Cached: 61916 kB SwapCached: 844 kB Active: 76880 kB Inactive: 23072 kB HighTotal: 131008 kB HighFree: 66192 kB LowTotal: 903652 kB LowFree: 835964 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 26908 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:40:40 (client local time) WITH STATUS 0 IN 449.549 SECONDS stats: 2809 7 449.549 0
c Parsing PB file... c PARSE ERROR! [line 2754] 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/6330/stat): 6330 (minisat+_script) R 6329 6330 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844129878 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/6330/statm): 174 3 169 147 0 27 0 [pid=6330] 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=6331 New process pid=6332 New process pid=6333 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 One traced child (pid=6332) exited with status: 0 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=6333) exited with status: 0 One traced child (pid=6331) exited with status: 0 New process pid=6334 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb One traced child (pid=6334) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=6335 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-scsd8.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 4988 0 0 0 936 27 0 0 25 0 1 0 1844129886 23150592 4687 4294967295 134512640 135167914 3221224448 3221222652 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6335/statm): 5652 4687 162 162 0 5490 0 [pid=6335] vsize: 22608 Current children cumulated CPU time (s) 9.65 Current children cumulated vsize (Kb) 24736 [startup+20.0046 s] Raw data (loadavg): 0.94 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 7202 0 0 0 1902 42 0 0 25 0 1 0 1844129886 32219136 6901 4294967295 134512640 135167914 3221224448 3221223016 134846935 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 7866 6901 162 162 0 7704 0 [pid=6335] vsize: 31464 Current children cumulated CPU time (s) 19.46 Current children cumulated vsize (Kb) 33592 [startup+30.0065 s] Raw data (loadavg): 0.95 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 9469 0 0 0 2873 56 0 0 25 0 1 0 1844129886 41504768 9168 4294967295 134512640 135167914 3221224448 3221222724 134845880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 10133 9168 162 162 0 9971 0 [pid=6335] vsize: 40532 Current children cumulated CPU time (s) 29.31 Current children cumulated vsize (Kb) 42660 [startup+40.0074 s] Raw data (loadavg): 0.96 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 12873 0 0 0 3833 77 0 0 25 0 1 0 1844129886 53448704 12088 4294967295 134512640 135167914 3221224448 3221223132 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6335/statm): 13049 12088 162 162 0 12887 0 [pid=6335] vsize: 52196 Current children cumulated CPU time (s) 39.12 Current children cumulated vsize (Kb) 54324 [startup+50.0084 s] Raw data (loadavg): 0.96 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 18386 0 0 0 4788 101 0 0 25 0 1 0 1844129886 74674176 17271 4294967295 134512640 135167914 3221224448 3221116640 134625423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 18231 17271 162 162 0 18069 0 [pid=6335] vsize: 72924 Current children cumulated CPU time (s) 48.91 Current children cumulated vsize (Kb) 75052 [startup+60.0093 s] Raw data (loadavg): 0.97 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 24999 0 0 0 5733 128 0 0 25 0 1 0 1844129886 99061760 23225 4294967295 134512640 135167914 3221224448 3221119980 134625005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 24185 23225 162 162 0 24023 0 [pid=6335] vsize: 96740 Current children cumulated CPU time (s) 58.63 Current children cumulated vsize (Kb) 98868 [startup+70.0102 s] Raw data (loadavg): 0.97 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 29529 0 0 0 6684 149 0 0 25 0 1 0 1844129886 112218112 26437 4294967295 134512640 135167914 3221224448 3221116096 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 27397 26437 162 162 0 27235 0 [pid=6335] vsize: 109588 Current children cumulated CPU time (s) 68.35 Current children cumulated vsize (Kb) 111716 [startup+80.0121 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 38331 0 0 0 7632 179 0 0 25 0 1 0 1844129886 137469952 32602 4294967295 134512640 135167914 3221224448 3221117772 134619926 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 33562 32602 162 162 0 33400 0 [pid=6335] vsize: 134248 Current children cumulated CPU time (s) 78.13 Current children cumulated vsize (Kb) 136376 [startup+90.013 s] Raw data (loadavg): 0.98 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 42926 0 0 0 8579 201 0 0 25 0 1 0 1844129886 156295168 37197 4294967295 134512640 135167914 3221224448 3221115996 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6335/statm): 38158 37197 162 162 0 37996 0 [pid=6335] vsize: 152632 Current children cumulated CPU time (s) 87.82 Current children cumulated vsize (Kb) 154760 [startup+100.013 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 47486 0 0 0 9526 224 0 0 25 0 1 0 1844129886 174968832 41757 4294967295 134512640 135167914 3221224448 3221116208 134619122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 42717 41757 162 162 0 42555 0 [pid=6335] vsize: 170868 Current children cumulated CPU time (s) 97.52 Current children cumulated vsize (Kb) 172996 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 51996 0 0 0 10476 244 0 0 25 0 1 0 1844129886 193441792 46267 4294967295 134512640 135167914 3221224448 3221116156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6335/statm): 47227 46267 162 162 0 47065 0 [pid=6335] vsize: 188908 Current children cumulated CPU time (s) 107.22 Current children cumulated vsize (Kb) 191036 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 65107 0 0 0 11424 280 0 0 25 0 1 0 1844129886 225546240 54105 4294967295 134512640 135167914 3221224448 3221116400 134849061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6335/statm): 55065 54105 162 162 0 54903 0 [pid=6335] vsize: 220260 Current children cumulated CPU time (s) 117.06 Current children cumulated vsize (Kb) 222388 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 69672 0 0 0 12376 302 0 0 25 0 1 0 1844129886 244244480 58670 4294967295 134512640 135167914 3221224448 3221116564 134697266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 59630 58670 162 162 0 59468 0 [pid=6335] vsize: 238520 Current children cumulated CPU time (s) 126.8 Current children cumulated vsize (Kb) 240648 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 74204 0 0 0 13327 325 0 0 25 0 1 0 1844129886 262807552 63202 4294967295 134512640 135167914 3221224448 3221120256 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 64162 63202 162 162 0 64000 0 [pid=6335] vsize: 256648 Current children cumulated CPU time (s) 136.54 Current children cumulated vsize (Kb) 258776 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 78674 0 0 0 14276 346 0 0 25 0 1 0 1844129886 281116672 67672 4294967295 134512640 135167914 3221224448 3221115888 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6335/statm): 68632 67672 162 162 0 68470 0 [pid=6335] vsize: 274528 Current children cumulated CPU time (s) 146.24 Current children cumulated vsize (Kb) 276656 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 83175 0 0 0 15226 367 0 0 25 0 1 0 1844129886 299552768 72173 4294967295 134512640 135167914 3221224448 3221119296 134849096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 73133 72173 162 162 0 72971 0 [pid=6335] vsize: 292532 Current children cumulated CPU time (s) 155.95 Current children cumulated vsize (Kb) 294660 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 87622 0 0 0 16176 387 0 0 25 0 1 0 1844129886 317767680 76620 4294967295 134512640 135167914 3221224448 3221119924 134697371 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6335/statm): 77580 76620 162 162 0 77418 0 [pid=6335] vsize: 310320 Current children cumulated CPU time (s) 165.65 Current children cumulated vsize (Kb) 312448 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 92044 0 0 0 17129 408 0 0 25 0 1 0 1844129886 335880192 81042 4294967295 134512640 135167914 3221224448 3221115440 134843426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 82002 81042 162 162 0 81840 0 [pid=6335] vsize: 328008 Current children cumulated CPU time (s) 175.39 Current children cumulated vsize (Kb) 330136 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 96397 0 0 0 18078 428 0 0 25 0 1 0 1844129886 353710080 85395 4294967295 134512640 135167914 3221224448 3221117460 134697377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 86355 85395 162 162 0 86193 0 [pid=6335] vsize: 345420 Current children cumulated CPU time (s) 185.08 Current children cumulated vsize (Kb) 347548 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 118050 0 0 0 19023 480 0 0 25 0 1 0 1844129886 399204352 96502 4294967295 134512640 135167914 3221224448 3221118288 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6335/statm): 97462 96502 162 162 0 97300 0 [pid=6335] vsize: 389848 Current children cumulated CPU time (s) 195.05 Current children cumulated vsize (Kb) 391976 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 122674 0 0 0 19971 503 0 0 25 0 1 0 1844129886 418144256 101126 4294967295 134512640 135167914 3221224448 3221116520 134846921 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 102086 101126 162 162 0 101924 0 [pid=6335] vsize: 408344 Current children cumulated CPU time (s) 204.76 Current children cumulated vsize (Kb) 410472 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 127302 0 0 0 20918 524 0 0 25 0 1 0 1844129886 437104640 105754 4294967295 134512640 135167914 3221224448 3221115520 134847159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 106715 105754 162 162 0 106553 0 [pid=6335] vsize: 426860 Current children cumulated CPU time (s) 214.44 Current children cumulated vsize (Kb) 428988 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 131867 0 0 0 21867 546 0 0 25 0 1 0 1844129886 455798784 110319 4294967295 134512640 135167914 3221224448 3221116448 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 111279 110319 162 162 0 111117 0 [pid=6335] vsize: 445116 Current children cumulated CPU time (s) 224.15 Current children cumulated vsize (Kb) 447244 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 136442 0 0 0 22817 566 0 0 25 0 1 0 1844129886 474537984 114894 4294967295 134512640 135167914 3221224448 3221116224 134844720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 115854 114894 162 162 0 115692 0 [pid=6335] vsize: 463416 Current children cumulated CPU time (s) 233.85 Current children cumulated vsize (Kb) 465544 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 140987 0 0 0 23766 588 0 0 25 0 1 0 1844129886 493158400 119439 4294967295 134512640 135167914 3221224448 3221115932 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6335/statm): 120400 119439 162 162 0 120238 0 [pid=6335] vsize: 481600 Current children cumulated CPU time (s) 243.56 Current children cumulated vsize (Kb) 483728 [startup+260.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 145525 0 0 0 24712 610 0 0 25 0 1 0 1844129886 511741952 123977 4294967295 134512640 135167914 3221224448 3221118428 134694551 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 124937 123977 162 162 0 124775 0 [pid=6335] vsize: 499748 Current children cumulated CPU time (s) 253.24 Current children cumulated vsize (Kb) 501876 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 150080 0 0 0 25659 633 0 0 25 0 1 0 1844129886 530399232 128532 4294967295 134512640 135167914 3221224448 3221115748 134620525 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 129492 128532 162 162 0 129330 0 [pid=6335] vsize: 517968 Current children cumulated CPU time (s) 262.94 Current children cumulated vsize (Kb) 520096 [startup+280.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 154676 0 0 0 26605 655 0 0 25 0 1 0 1844129886 549224448 133128 4294967295 134512640 135167914 3221224448 3221116512 134843068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 134088 133128 162 162 0 133926 0 [pid=6335] vsize: 536352 Current children cumulated CPU time (s) 272.62 Current children cumulated vsize (Kb) 538480 [startup+290.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 159177 0 0 0 27557 677 0 0 25 0 1 0 1844129886 567660544 137629 4294967295 134512640 135167914 3221224448 3221115484 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6335/statm): 138589 137629 162 162 0 138427 0 [pid=6335] vsize: 554356 Current children cumulated CPU time (s) 282.36 Current children cumulated vsize (Kb) 556484 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 163683 0 0 0 28508 697 0 0 25 0 1 0 1844129886 586117120 142135 4294967295 134512640 135167914 3221224448 3221115904 134696140 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 143095 142135 162 162 0 142933 0 [pid=6335] vsize: 572380 Current children cumulated CPU time (s) 292.07 Current children cumulated vsize (Kb) 574508 [startup+310.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 168138 0 0 0 29460 715 0 0 25 0 1 0 1844129886 604364800 146590 4294967295 134512640 135167914 3221224448 3221117296 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 147550 146590 162 162 0 147388 0 [pid=6335] vsize: 590200 Current children cumulated CPU time (s) 301.77 Current children cumulated vsize (Kb) 592328 [startup+320.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 172587 0 0 0 30409 736 0 0 25 0 1 0 1844129886 622587904 151039 4294967295 134512640 135167914 3221224448 3221119516 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 151999 151039 162 162 0 151837 0 [pid=6335] vsize: 607996 Current children cumulated CPU time (s) 311.47 Current children cumulated vsize (Kb) 610124 [startup+330.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 177052 0 0 0 31359 757 0 0 25 0 1 0 1844129886 640876544 155504 4294967295 134512640 135167914 3221224448 3221115968 134722524 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 156464 155504 162 162 0 156302 0 [pid=6335] vsize: 625856 Current children cumulated CPU time (s) 321.18 Current children cumulated vsize (Kb) 627984 [startup+340.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 207059 0 0 0 32254 834 0 0 25 0 1 0 1844129886 830418944 185512 4294967295 134512640 135167914 3221224448 3221118880 134625368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 202739 185512 162 162 0 202577 0 [pid=6335] vsize: 810956 Current children cumulated CPU time (s) 330.9 Current children cumulated vsize (Kb) 813084 [startup+350.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 223327 0 0 0 33217 871 0 0 25 0 1 0 1844129886 830418944 201779 4294967295 134512640 135167914 3221224448 3221118704 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6335/statm): 202739 201779 162 162 0 202577 0 [pid=6335] vsize: 810956 Current children cumulated CPU time (s) 340.9 Current children cumulated vsize (Kb) 813084 [startup+360.039 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 224761 0 0 0 34199 881 0 0 25 0 1 0 1844129886 749907968 182122 4294967295 134512640 135167914 3221224448 3221115996 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6335/statm): 183083 182122 162 162 0 182921 0 [pid=6335] vsize: 732332 Current children cumulated CPU time (s) 350.82 Current children cumulated vsize (Kb) 734460 [startup+370.04 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 229380 0 0 0 35146 903 0 0 25 0 1 0 1844129886 768827392 186741 4294967295 134512640 135167914 3221224448 3221115676 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6335/statm): 187702 186741 162 162 0 187540 0 [pid=6335] vsize: 750808 Current children cumulated CPU time (s) 360.51 Current children cumulated vsize (Kb) 752936 [startup+380.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 234057 0 0 0 36090 925 0 0 25 0 1 0 1844129886 787980288 191418 4294967295 134512640 135167914 3221224448 3221117788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/6335/statm): 192378 191418 162 162 0 192216 0 [pid=6335] vsize: 769512 Current children cumulated CPU time (s) 370.17 Current children cumulated vsize (Kb) 771640 [startup+390.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 238696 0 0 0 37039 946 0 0 25 0 1 0 1844129886 806981632 196057 4294967295 134512640 135167914 3221224448 3221116828 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 197017 196057 162 162 0 196855 0 [pid=6335] vsize: 788068 Current children cumulated CPU time (s) 379.87 Current children cumulated vsize (Kb) 790196 [startup+400.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 243328 0 0 0 37986 968 0 0 25 0 1 0 1844129886 825954304 200689 4294967295 134512640 135167914 3221224448 3221116224 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 201649 200689 162 162 0 201487 0 [pid=6335] vsize: 806596 Current children cumulated CPU time (s) 389.56 Current children cumulated vsize (Kb) 808724 [startup+410.045 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 247977 0 0 0 38937 990 0 0 25 0 1 0 1844129886 844996608 205338 4294967295 134512640 135167914 3221224448 3221118044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6335/statm): 206298 205338 162 162 0 206136 0 [pid=6335] vsize: 825192 Current children cumulated CPU time (s) 399.29 Current children cumulated vsize (Kb) 827320 [startup+420.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 252558 0 0 0 39885 1011 0 0 25 0 1 0 1844129886 863760384 209919 4294967295 134512640 135167914 3221224448 3221117968 134849082 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 210879 209919 162 162 0 210717 0 [pid=6335] vsize: 843516 Current children cumulated CPU time (s) 408.98 Current children cumulated vsize (Kb) 845644 [startup+430.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 257137 0 0 0 40834 1031 0 0 25 0 1 0 1844129886 882515968 214498 4294967295 134512640 135167914 3221224448 3221120896 134621017 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 215458 214498 162 162 0 215296 0 [pid=6335] vsize: 861832 Current children cumulated CPU time (s) 418.67 Current children cumulated vsize (Kb) 863960 [startup+440.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 261773 0 0 0 41786 1052 0 0 25 0 1 0 1844129886 901505024 219134 4294967295 134512640 135167914 3221224448 3221117072 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 220094 219134 162 162 0 219932 0 [pid=6335] vsize: 880376 Current children cumulated CPU time (s) 428.4 Current children cumulated vsize (Kb) 882504 [startup+450.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 266353 0 0 0 42734 1074 0 0 25 0 1 0 1844129886 920264704 223714 4294967295 134512640 135167914 3221224448 3221118416 134843030 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 224674 223714 162 162 0 224512 0 [pid=6335] vsize: 898696 Current children cumulated CPU time (s) 438.1 Current children cumulated vsize (Kb) 900824 [startup+460.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) R 6330 6330 31027 0 -1 0 270884 0 12 0 43667 1099 0 0 25 0 1 0 1844129886 938737664 227795 4294967295 134512640 135167914 3221224448 3221118132 134843000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6335/statm): 229184 227795 162 162 0 229022 0 [pid=6335] vsize: 916736 Current children cumulated CPU time (s) 447.68 Current children cumulated vsize (Kb) 918864 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+461.67 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 6335 Raw data (/proc/6330/stat): 6330 (minisat+_script) S 6329 6330 31027 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844129878 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6330/statm): 532 234 485 147 0 385 0 [pid=6330] vsize: 2128 Raw data (/proc/6335/stat): 6335 (minisat+_bignum) T 6330 6330 31027 0 -1 0 271693 0 31 0 43808 1104 0 0 25 0 1 0 1844129886 941543424 228528 4294967295 134512640 135167914 3221224448 3221118492 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6335/statm): 229869 228528 162 162 0 229707 0 [pid=6335] vsize: 919476 Current children cumulated CPU time (s) 449.14 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -6330 Sleeping 2 seconds One traced child (pid=6330) ended because it received signal 15 (SIGTERM) One traced child (pid=6335) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 462.094 CPU time (s): 449.549 CPU user time (s): 438.087 CPU system time (s): 11.4613 CPU usage (%): 97.2851 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !