Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-scsd6.opb |
MD5SUM | b052177a073d2d8c92d9603ed92c19ee |
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 | 40500 |
Biggest coefficient in the objective function | 240095970606448640 |
Number of bits for the biggest coefficient in the objective function | 58 |
Sum of the numbers in the objective function | 319188057892705075200 |
Number of bits of the sum of numbers in the objective function | 69 |
Biggest number in a constraint | 240095970606448640 |
Number of bits of the biggest number in a constraint | 58 |
Biggest sum of numbers in a constraint | 319188057892705075200 |
Number of bits of the biggest sum of numbers | 69 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 40500 |
Total number of constraints | 147 |
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 | 147 |
Minimum length of a constraint | 600 |
Maximum length of a constraint | 1200 |
LAUNCH ON wulflinc30 THE 2005-09-18 20:31:58 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2808 boxname=wulflinc30 idbench=464 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b052177a073d2d8c92d9603ed92c19ee /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-scsd6.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-scsd6.opb IDLAUNCH: 2808 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 899248 kB Buffers: 37632 kB Cached: 67388 kB SwapCached: 788 kB Active: 71220 kB Inactive: 36524 kB HighTotal: 131008 kB HighFree: 62804 kB LowTotal: 903652 kB LowFree: 836444 kB SwapTotal: 2097892 kB SwapFree: 2096636 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5732 kB Slab: 22108 kB Committed_AS: 64172 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:40:28 (client local time) WITH STATUS 0 IN 497.311 SECONDS stats: 2808 7 497.311 0
c Parsing PB file... c PARSE ERROR! [line 1354] 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/14791/stat): 14791 (minisat+_script) R 14790 14791 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844145173 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/14791/statm): 174 3 169 147 0 27 0 [pid=14791] 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=14792 New process pid=14793 New process pid=14794 execve syscall for /bin/sed executable One traced child (pid=14793) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=14794) exited with status: 0 One traced child (pid=14792) exited with status: 0 New process pid=14795 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-scsd6.opb One traced child (pid=14795) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=14796 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-scsd6.opb [startup+10.0042 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 3645 0 0 0 953 19 0 0 25 0 1 0 1844145180 16490496 3549 4294967295 134512640 135167914 3221224448 3221223232 134691301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14796/statm): 4026 3549 162 162 0 3864 0 [pid=14796] vsize: 16104 Current children cumulated CPU time (s) 9.74 Current children cumulated vsize (Kb) 18232 [startup+20.005 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 5846 0 0 0 1919 35 0 0 25 0 1 0 1844145180 25501696 5750 4294967295 134512640 135167914 3221224448 3221222216 134693719 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 6226 5750 162 162 0 6064 0 [pid=14796] vsize: 24904 Current children cumulated CPU time (s) 19.56 Current children cumulated vsize (Kb) 27032 [startup+30.0058 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 11145 0 0 0 2873 58 0 0 25 0 1 0 1844145180 43843584 10233 4294967295 134512640 135167914 3221224448 3221063924 134697076 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 10704 10233 162 162 0 10542 0 [pid=14796] vsize: 42816 Current children cumulated CPU time (s) 29.33 Current children cumulated vsize (Kb) 44944 [startup+40.0066 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 16114 0 0 0 3830 78 0 0 25 0 1 0 1844145180 61497344 14543 4294967295 134512640 135167914 3221224448 3221062544 134849143 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 15014 14543 162 162 0 14852 0 [pid=14796] vsize: 60056 Current children cumulated CPU time (s) 39.1 Current children cumulated vsize (Kb) 62184 [startup+50.0084 s] Raw data (loadavg): 0.96 0.96 0.91 3/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 22343 0 0 0 4785 100 0 0 25 0 1 0 1844145180 81612800 19454 4294967295 134512640 135167914 3221224448 3221062012 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 19925 19454 162 162 0 19763 0 [pid=14796] vsize: 79700 Current children cumulated CPU time (s) 48.87 Current children cumulated vsize (Kb) 81828 [startup+60.0092 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 26230 0 0 0 5742 120 0 0 25 0 1 0 1844145180 97533952 23341 4294967295 134512640 135167914 3221224448 3221061824 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 23812 23341 162 162 0 23650 0 [pid=14796] vsize: 95248 Current children cumulated CPU time (s) 58.64 Current children cumulated vsize (Kb) 97376 [startup+70.009 s] Raw data (loadavg): 0.97 0.96 0.91 1/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 34735 0 0 0 6694 148 0 0 25 0 1 0 1844145180 121569280 29209 4294967295 134512640 135167914 3221224448 3221062268 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 29680 29209 162 162 0 29518 0 [pid=14796] vsize: 118720 Current children cumulated CPU time (s) 68.44 Current children cumulated vsize (Kb) 120848 [startup+80.0098 s] Raw data (loadavg): 0.98 0.96 0.91 1/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 38735 0 0 0 7649 166 0 0 25 0 1 0 1844145180 137957376 33209 4294967295 134512640 135167914 3221224448 3221062012 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 33681 33209 162 162 0 33519 0 [pid=14796] vsize: 134724 Current children cumulated CPU time (s) 78.17 Current children cumulated vsize (Kb) 136852 [startup+90.0106 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 42692 0 0 0 8607 184 0 0 25 0 1 0 1844145180 154161152 37166 4294967295 134512640 135167914 3221224448 3221062648 134849087 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 37637 37166 162 162 0 37475 0 [pid=14796] vsize: 150548 Current children cumulated CPU time (s) 87.93 Current children cumulated vsize (Kb) 152676 [startup+100.011 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 46793 0 0 0 9561 203 0 0 25 0 1 0 1844145180 170958848 41267 4294967295 134512640 135167914 3221224448 3221062472 134847205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 41738 41267 162 162 0 41576 0 [pid=14796] vsize: 166952 Current children cumulated CPU time (s) 97.66 Current children cumulated vsize (Kb) 169080 [startup+110.012 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 59571 0 0 0 10511 237 0 0 25 0 1 0 1844145180 201699328 48772 4294967295 134512640 135167914 3221224448 3221062356 134697405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 49243 48772 162 162 0 49081 0 [pid=14796] vsize: 196972 Current children cumulated CPU time (s) 107.5 Current children cumulated vsize (Kb) 199100 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 63689 0 0 0 11465 257 0 0 25 0 1 0 1844145180 218566656 52890 4294967295 134512640 135167914 3221224448 3221062300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 53361 52890 162 162 0 53199 0 [pid=14796] vsize: 213444 Current children cumulated CPU time (s) 117.24 Current children cumulated vsize (Kb) 215572 [startup+130.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 67652 0 0 0 12422 274 0 0 25 0 1 0 1844145180 234799104 56853 4294967295 134512640 135167914 3221224448 3221063808 134844775 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 57324 56853 162 162 0 57162 0 [pid=14796] vsize: 229296 Current children cumulated CPU time (s) 126.98 Current children cumulated vsize (Kb) 231424 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 71537 0 0 0 13379 290 0 0 25 0 1 0 1844145180 250712064 60738 4294967295 134512640 135167914 3221224448 3221064284 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 61209 60738 162 162 0 61047 0 [pid=14796] vsize: 244836 Current children cumulated CPU time (s) 136.71 Current children cumulated vsize (Kb) 246964 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 75511 0 0 0 14335 308 0 0 25 0 1 0 1844145180 266989568 64712 4294967295 134512640 135167914 3221224448 3221063040 134695970 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14796/statm): 65183 64712 162 162 0 65021 0 [pid=14796] vsize: 260732 Current children cumulated CPU time (s) 146.45 Current children cumulated vsize (Kb) 262860 [startup+160.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 79604 0 0 0 15288 327 0 0 25 0 1 0 1844145180 283754496 68805 4294967295 134512640 135167914 3221224448 3221062640 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 69276 68805 162 162 0 69114 0 [pid=14796] vsize: 277104 Current children cumulated CPU time (s) 156.17 Current children cumulated vsize (Kb) 279232 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 83526 0 0 0 16245 345 0 0 25 0 1 0 1844145180 299819008 72727 4294967295 134512640 135167914 3221224448 3221062496 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 73198 72727 162 162 0 73036 0 [pid=14796] vsize: 292792 Current children cumulated CPU time (s) 165.92 Current children cumulated vsize (Kb) 294920 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 87461 0 0 0 17203 363 0 0 25 0 1 0 1844145180 315936768 76662 4294967295 134512640 135167914 3221224448 3221062660 134620326 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 77133 76662 162 162 0 76971 0 [pid=14796] vsize: 308532 Current children cumulated CPU time (s) 175.68 Current children cumulated vsize (Kb) 310660 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 111851 0 0 0 18118 428 0 0 25 0 1 0 1844145180 415838208 101052 4294967295 134512640 135167914 3221224448 3221063280 134694428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14796/statm): 101523 101052 162 162 0 101361 0 [pid=14796] vsize: 406092 Current children cumulated CPU time (s) 185.48 Current children cumulated vsize (Kb) 408220 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 113255 0 0 0 19101 437 0 0 25 0 1 0 1844145180 378392576 91910 4294967295 134512640 135167914 3221224448 3221061980 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 92381 91910 162 162 0 92219 0 [pid=14796] vsize: 369524 Current children cumulated CPU time (s) 195.4 Current children cumulated vsize (Kb) 371652 [startup+210.019 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 117356 0 0 0 20058 455 0 0 25 0 1 0 1844145180 395190272 96011 4294967295 134512640 135167914 3221224448 3221061564 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 96482 96011 162 162 0 96320 0 [pid=14796] vsize: 385928 Current children cumulated CPU time (s) 205.15 Current children cumulated vsize (Kb) 388056 [startup+220.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 121587 0 0 0 21007 476 0 0 25 0 1 0 1844145180 412520448 100242 4294967295 134512640 135167914 3221224448 3221061756 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 100713 100242 162 162 0 100551 0 [pid=14796] vsize: 402852 Current children cumulated CPU time (s) 214.85 Current children cumulated vsize (Kb) 404980 [startup+230.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 125774 0 0 0 21961 495 0 0 25 0 1 0 1844145180 429670400 104429 4294967295 134512640 135167914 3221224448 3221067136 134619190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 104900 104429 162 162 0 104738 0 [pid=14796] vsize: 419600 Current children cumulated CPU time (s) 224.58 Current children cumulated vsize (Kb) 421728 [startup+240.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 129985 0 0 0 22916 513 0 0 25 0 1 0 1844145180 446918656 108640 4294967295 134512640 135167914 3221224448 3221061792 134844760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 109111 108640 162 162 0 108949 0 [pid=14796] vsize: 436444 Current children cumulated CPU time (s) 234.31 Current children cumulated vsize (Kb) 438572 [startup+250.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 133939 0 0 0 23874 531 0 0 25 0 1 0 1844145180 463114240 112594 4294967295 134512640 135167914 3221224448 3221063640 134722513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 113065 112594 162 162 0 112903 0 [pid=14796] vsize: 452260 Current children cumulated CPU time (s) 244.07 Current children cumulated vsize (Kb) 454388 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 137996 0 0 0 24828 548 0 0 25 0 1 0 1844145180 479731712 116651 4294967295 134512640 135167914 3221224448 3221063680 134845903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 117122 116651 162 162 0 116960 0 [pid=14796] vsize: 468488 Current children cumulated CPU time (s) 253.78 Current children cumulated vsize (Kb) 470616 [startup+270.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 142016 0 0 0 25785 566 0 0 25 0 1 0 1844145180 496197632 120671 4294967295 134512640 135167914 3221224448 3221062784 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 121142 120671 162 162 0 120980 0 [pid=14796] vsize: 484568 Current children cumulated CPU time (s) 263.53 Current children cumulated vsize (Kb) 486696 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 145883 0 0 0 26743 584 0 0 25 0 1 0 1844145180 512036864 124538 4294967295 134512640 135167914 3221224448 3221062268 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 125009 124538 162 162 0 124847 0 [pid=14796] vsize: 500036 Current children cumulated CPU time (s) 273.29 Current children cumulated vsize (Kb) 502164 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 149806 0 0 0 27702 601 0 0 25 0 1 0 1844145180 528113664 128461 4294967295 134512640 135167914 3221224448 3221062336 134695201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 128934 128461 162 162 0 128772 0 [pid=14796] vsize: 515736 Current children cumulated CPU time (s) 283.05 Current children cumulated vsize (Kb) 517864 [startup+300.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 153720 0 0 0 28662 618 0 0 25 0 1 0 1844145180 544145408 132375 4294967295 134512640 135167914 3221224448 3221063388 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 132848 132375 162 162 0 132686 0 [pid=14796] vsize: 531392 Current children cumulated CPU time (s) 292.82 Current children cumulated vsize (Kb) 533520 [startup+310.026 s] Raw data (loadavg): 1.07 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 157703 0 0 0 29620 635 0 0 25 0 1 0 1844145180 560455680 136358 4294967295 134512640 135167914 3221224448 3221062048 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 136830 136358 162 162 0 136668 0 [pid=14796] vsize: 547320 Current children cumulated CPU time (s) 302.57 Current children cumulated vsize (Kb) 549448 [startup+320.026 s] Raw data (loadavg): 1.06 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 161476 0 0 0 30579 652 0 0 25 0 1 0 1844145180 575909888 140131 4294967295 134512640 135167914 3221224448 3221063964 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 140603 140131 162 162 0 140441 0 [pid=14796] vsize: 562412 Current children cumulated CPU time (s) 312.33 Current children cumulated vsize (Kb) 564540 [startup+330.027 s] Raw data (loadavg): 1.05 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 165239 0 0 0 31537 668 0 0 25 0 1 0 1844145180 591323136 143894 4294967295 134512640 135167914 3221224448 3221063968 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 144366 143894 162 162 0 144204 0 [pid=14796] vsize: 577464 Current children cumulated CPU time (s) 322.07 Current children cumulated vsize (Kb) 579592 [startup+340.026 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 169099 0 0 0 32494 686 0 0 25 0 1 0 1844145180 607133696 147754 4294967295 134512640 135167914 3221224448 3221063412 134849220 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 148226 147754 162 162 0 148064 0 [pid=14796] vsize: 592904 Current children cumulated CPU time (s) 331.82 Current children cumulated vsize (Kb) 595032 [startup+350.027 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 172900 0 0 0 33451 704 0 0 25 0 1 0 1844145180 622702592 151555 4294967295 134512640 135167914 3221224448 3221062784 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 152027 151555 162 162 0 151865 0 [pid=14796] vsize: 608108 Current children cumulated CPU time (s) 341.57 Current children cumulated vsize (Kb) 610236 [startup+360.028 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 217630 0 0 0 34324 813 0 0 25 0 1 0 1844145180 805916672 196285 4294967295 134512640 135167914 3221224448 3221063312 134625468 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 196757 196285 162 162 0 196595 0 [pid=14796] vsize: 787028 Current children cumulated CPU time (s) 351.39 Current children cumulated vsize (Kb) 789156 [startup+370.028 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 217630 0 0 0 35325 813 0 0 25 0 1 0 1844145180 805916672 196285 4294967295 134512640 135167914 3221224448 3221063264 134849071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 196757 196285 162 162 0 196595 0 [pid=14796] vsize: 787028 Current children cumulated CPU time (s) 361.4 Current children cumulated vsize (Kb) 789156 [startup+380.029 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 220159 0 0 0 36291 831 0 0 25 0 1 0 1844145180 729886720 177723 4294967295 134512640 135167914 3221224448 3221062464 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 178195 177723 162 162 0 178033 0 [pid=14796] vsize: 712780 Current children cumulated CPU time (s) 371.24 Current children cumulated vsize (Kb) 714908 [startup+390.029 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 224243 0 0 0 37245 851 0 0 25 0 1 0 1844145180 746614784 181807 4294967295 134512640 135167914 3221224448 3221063776 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 182279 181807 162 162 0 182117 0 [pid=14796] vsize: 729116 Current children cumulated CPU time (s) 380.98 Current children cumulated vsize (Kb) 731244 [startup+400.03 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 228414 0 0 0 38198 873 0 0 25 0 1 0 1844145180 763699200 185978 4294967295 134512640 135167914 3221224448 3221062048 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 186450 185978 162 162 0 186288 0 [pid=14796] vsize: 745800 Current children cumulated CPU time (s) 390.73 Current children cumulated vsize (Kb) 747928 [startup+410.031 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 232582 0 0 0 39149 894 0 0 25 0 1 0 1844145180 780771328 190146 4294967295 134512640 135167914 3221224448 3221063808 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 190618 190146 162 162 0 190456 0 [pid=14796] vsize: 762472 Current children cumulated CPU time (s) 400.45 Current children cumulated vsize (Kb) 764600 [startup+420.031 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 236645 0 0 0 40105 914 0 0 25 0 1 0 1844145180 797413376 194209 4294967295 134512640 135167914 3221224448 3221062492 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 194681 194209 162 162 0 194519 0 [pid=14796] vsize: 778724 Current children cumulated CPU time (s) 410.21 Current children cumulated vsize (Kb) 780852 [startup+430.032 s] Raw data (loadavg): 1.01 0.99 0.92 1/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 240691 0 0 0 41060 933 0 0 25 0 1 0 1844145180 813985792 198255 4294967295 134512640 135167914 3221224448 3221061724 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 198727 198255 162 162 0 198565 0 [pid=14796] vsize: 794908 Current children cumulated CPU time (s) 419.95 Current children cumulated vsize (Kb) 797036 [startup+440.032 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 244642 0 0 0 42015 951 0 0 25 0 1 0 1844145180 830169088 202206 4294967295 134512640 135167914 3221224448 3221062300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 202678 202206 162 162 0 202516 0 [pid=14796] vsize: 810712 Current children cumulated CPU time (s) 429.68 Current children cumulated vsize (Kb) 812840 [startup+450.033 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 248629 0 0 0 42970 970 0 0 25 0 1 0 1844145180 846499840 206193 4294967295 134512640 135167914 3221224448 3221063936 134695622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 206665 206193 162 162 0 206503 0 [pid=14796] vsize: 826660 Current children cumulated CPU time (s) 439.42 Current children cumulated vsize (Kb) 828788 [startup+460.034 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 252587 0 0 0 43928 990 0 0 25 0 1 0 1844145180 862711808 210151 4294967295 134512640 135167914 3221224448 3221062112 134845002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 210623 210151 162 162 0 210461 0 [pid=14796] vsize: 842492 Current children cumulated CPU time (s) 449.2 Current children cumulated vsize (Kb) 844620 [startup+470.034 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 256512 0 0 0 44885 1006 0 0 20 0 1 0 1844145180 878788608 214076 4294967295 134512640 135167914 3221224448 3221064672 134619257 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 214548 214076 162 162 0 214386 0 [pid=14796] vsize: 858192 Current children cumulated CPU time (s) 458.93 Current children cumulated vsize (Kb) 860320 [startup+480.035 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 260427 0 0 0 45840 1024 0 0 25 0 1 0 1844145180 894824448 217991 4294967295 134512640 135167914 3221224448 3221063504 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14796/statm): 218463 217991 162 162 0 218301 0 [pid=14796] vsize: 873852 Current children cumulated CPU time (s) 468.66 Current children cumulated vsize (Kb) 875980 [startup+490.035 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 264341 0 0 0 46797 1042 0 0 25 0 1 0 1844145180 910856192 221905 4294967295 134512640 135167914 3221224448 3221061788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 222377 221905 162 162 0 222215 0 [pid=14796] vsize: 889508 Current children cumulated CPU time (s) 478.41 Current children cumulated vsize (Kb) 891636 [startup+500.036 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) R 14791 14791 5245 0 -1 0 268280 0 11 0 47744 1059 0 0 24 0 1 0 1844145180 926822400 225695 4294967295 134512640 135167914 3221224448 3221062852 134849086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14796/statm): 226275 225695 162 162 0 226113 0 [pid=14796] vsize: 905100 Current children cumulated CPU time (s) 488.05 Current children cumulated vsize (Kb) 907228 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+509.276 s] Raw data (loadavg): 1.00 0.99 0.92 1/57 14796 Raw data (/proc/14791/stat): 14791 (minisat+_script) S 14790 14791 5245 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844145173 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14791/statm): 532 234 485 147 0 385 0 [pid=14791] vsize: 2128 Raw data (/proc/14796/stat): 14796 (minisat+_bignum) T 14791 14791 5245 0 -1 0 271941 0 24 0 48610 1077 0 0 25 0 1 0 1844145180 941543424 228918 4294967295 134512640 135167914 3221224448 3221062716 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14796/statm): 229869 228918 162 162 0 229707 0 [pid=14796] vsize: 919476 Current children cumulated CPU time (s) 496.89 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -14791 Sleeping 2 seconds One traced child (pid=14791) ended because it received signal 15 (SIGTERM) One traced child (pid=14796) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 509.704 CPU time (s): 497.311 CPU user time (s): 486.109 CPU system time (s): 11.2023 CPU usage (%): 97.5686 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !