Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-glass4.opb |
MD5SUM | 929651d54295ccab2bd7ed98e4ab5229 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 13303876395624 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 478 |
Biggest coefficient in the objective function | 536870912000000 |
Number of bits for the biggest coefficient in the objective function | 49 |
Sum of the numbers in the objective function | 1073761158741413 |
Number of bits of the sum of numbers in the objective function | 50 |
Biggest number in a constraint | 71583145981965762560 |
Number of bits of the biggest number in a constraint | 66 |
Biggest sum of numbers in a constraint | 303620978593259257856 |
Number of bits of the biggest sum of numbers | 69 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1259.64 |
Number of variables | 780 |
Total number of constraints | 707 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 338 |
Number of constraints which are nor clauses,nor cardinality constraints | 369 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 101 |
LAUNCH ON wulflinc4 THE 2005-09-19 03:40:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2912 boxname=wulflinc4 idbench=568 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 929651d54295ccab2bd7ed98e4ab5229 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-glass4.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-glass4.opb IDLAUNCH: 2912 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 906464 kB Buffers: 32516 kB Cached: 70104 kB SwapCached: 944 kB Active: 55108 kB Inactive: 50200 kB HighTotal: 131008 kB HighFree: 57932 kB LowTotal: 903652 kB LowFree: 848532 kB SwapTotal: 2097136 kB SwapFree: 2095644 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5692 kB Slab: 16992 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:46:55 (client local time) WITH STATUS 0 IN 401.296 SECONDS stats: 2912 7 401.296 0
c Parsing PB file... c PARSE ERROR! [line 326] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead...
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/30247/stat): 30247 (minisat+_script) R 30246 30247 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788484584 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/30247/statm): 174 3 169 147 0 27 0 [pid=30247] 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=30248 New process pid=30249 New process pid=30250 execve syscall for /bin/sed executable One traced child (pid=30249) 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=30250) exited with status: 0 One traced child (pid=30248) exited with status: 0 New process pid=30251 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-glass4.opb One traced child (pid=30251) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=30252 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-glass4.opb [startup+10.0043 s] Raw data (loadavg): 0.93 0.98 0.90 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 5536 0 0 0 942 22 0 0 25 0 1 0 1788484591 20459520 4902 4294967295 134512640 135167914 3221224448 3221201920 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30252/statm): 4995 4902 162 162 0 4833 0 [pid=30252] vsize: 19980 Current children cumulated CPU time (s) 9.65 Current children cumulated vsize (Kb) 22108 [startup+20.0051 s] Raw data (loadavg): 0.94 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 13852 0 0 0 1884 54 0 0 25 0 1 0 1788484591 51822592 12559 4294967295 134512640 135167914 3221224448 3221200624 134625468 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 12652 12559 162 162 0 12490 0 [pid=30252] vsize: 50608 Current children cumulated CPU time (s) 19.39 Current children cumulated vsize (Kb) 52736 [startup+30.006 s] Raw data (loadavg): 0.95 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 18799 0 0 0 2833 76 0 0 25 0 1 0 1788484591 66686976 16188 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 16281 16188 162 162 0 16119 0 [pid=30252] vsize: 65124 Current children cumulated CPU time (s) 29.1 Current children cumulated vsize (Kb) 67252 [startup+40.0069 s] Raw data (loadavg): 0.95 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 27979 0 0 0 3777 109 0 0 25 0 1 0 1788484591 93487104 22731 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 22824 22731 162 162 0 22662 0 [pid=30252] vsize: 91296 Current children cumulated CPU time (s) 38.87 Current children cumulated vsize (Kb) 93424 [startup+50.0088 s] Raw data (loadavg): 0.96 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 32628 0 0 0 4727 128 0 0 25 0 1 0 1788484591 112529408 27380 4294967295 134512640 135167914 3221224448 3221200640 134620615 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 27473 27380 162 162 0 27311 0 [pid=30252] vsize: 109892 Current children cumulated CPU time (s) 48.56 Current children cumulated vsize (Kb) 112020 [startup+60.0097 s] Raw data (loadavg): 0.97 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 37425 0 0 0 5673 152 0 0 25 0 1 0 1788484591 132177920 32177 4294967295 134512640 135167914 3221224448 3221200348 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 32270 32177 162 162 0 32108 0 [pid=30252] vsize: 129080 Current children cumulated CPU time (s) 58.26 Current children cumulated vsize (Kb) 131208 [startup+70.0106 s] Raw data (loadavg): 0.97 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 42273 0 0 0 6621 175 0 0 25 0 1 0 1788484591 152035328 37025 4294967295 134512640 135167914 3221224448 3221200396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 37118 37025 162 162 0 36956 0 [pid=30252] vsize: 148472 Current children cumulated CPU time (s) 67.97 Current children cumulated vsize (Kb) 150600 [startup+80.0116 s] Raw data (loadavg): 0.98 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 55749 0 0 0 7567 214 0 0 25 0 1 0 1788484591 185634816 45228 4294967295 134512640 135167914 3221224448 3221201500 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 45321 45228 162 162 0 45159 0 [pid=30252] vsize: 181284 Current children cumulated CPU time (s) 77.82 Current children cumulated vsize (Kb) 183412 [startup+90.0125 s] Raw data (loadavg): 0.98 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 60853 0 0 0 8511 235 0 0 25 0 1 0 1788484591 206540800 50332 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 50425 50332 162 162 0 50263 0 [pid=30252] vsize: 201700 Current children cumulated CPU time (s) 87.47 Current children cumulated vsize (Kb) 203828 [startup+100.013 s] Raw data (loadavg): 0.98 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 65675 0 0 0 9458 258 0 0 25 0 1 0 1788484591 226291712 55154 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 55247 55154 162 162 0 55085 0 [pid=30252] vsize: 220988 Current children cumulated CPU time (s) 97.17 Current children cumulated vsize (Kb) 223116 [startup+110.014 s] Raw data (loadavg): 0.98 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 70450 0 0 0 10411 278 0 0 25 0 1 0 1788484591 245850112 59929 4294967295 134512640 135167914 3221224448 3221201852 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 60022 59929 162 162 0 59860 0 [pid=30252] vsize: 240088 Current children cumulated CPU time (s) 106.9 Current children cumulated vsize (Kb) 242216 [startup+120.015 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 75247 0 0 0 11360 303 0 0 25 0 1 0 1788484591 265498624 64726 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 64819 64726 162 162 0 64657 0 [pid=30252] vsize: 259276 Current children cumulated CPU time (s) 116.64 Current children cumulated vsize (Kb) 261404 [startup+130.016 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 80090 0 0 0 12302 329 0 0 25 0 1 0 1788484591 285335552 69569 4294967295 134512640 135167914 3221224448 3221201664 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 69662 69569 162 162 0 69500 0 [pid=30252] vsize: 278648 Current children cumulated CPU time (s) 126.32 Current children cumulated vsize (Kb) 280776 [startup+140.017 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 84901 0 0 0 13249 349 0 0 25 0 1 0 1788484591 305041408 74380 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 74473 74380 162 162 0 74311 0 [pid=30252] vsize: 297892 Current children cumulated CPU time (s) 135.99 Current children cumulated vsize (Kb) 300020 [startup+150.018 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 106801 0 0 0 14193 401 0 0 25 0 1 0 1788484591 351547392 85734 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 85827 85734 162 162 0 85665 0 [pid=30252] vsize: 343308 Current children cumulated CPU time (s) 145.95 Current children cumulated vsize (Kb) 345436 [startup+160.019 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 111941 0 0 0 15138 424 0 0 25 0 1 0 1788484591 372600832 90874 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 90967 90874 162 162 0 90805 0 [pid=30252] vsize: 363868 Current children cumulated CPU time (s) 155.63 Current children cumulated vsize (Kb) 365996 [startup+170.019 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 116942 0 0 0 16083 447 0 0 25 0 1 0 1788484591 393084928 95875 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 95968 95875 162 162 0 95806 0 [pid=30252] vsize: 383872 Current children cumulated CPU time (s) 165.31 Current children cumulated vsize (Kb) 386000 [startup+180.02 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 121945 0 0 0 17025 472 0 0 25 0 1 0 1788484591 413577216 100878 4294967295 134512640 135167914 3221224448 3221200476 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 100971 100878 162 162 0 100809 0 [pid=30252] vsize: 403884 Current children cumulated CPU time (s) 174.98 Current children cumulated vsize (Kb) 406012 [startup+190.021 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 126910 0 0 0 17973 495 0 0 25 0 1 0 1788484591 433913856 105843 4294967295 134512640 135167914 3221224448 3221201148 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 105936 105843 162 162 0 105774 0 [pid=30252] vsize: 423744 Current children cumulated CPU time (s) 184.69 Current children cumulated vsize (Kb) 425872 [startup+200.022 s] Raw data (loadavg): 0.99 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 131898 0 0 0 18922 516 0 0 24 0 1 0 1788484591 454344704 110831 4294967295 134512640 135167914 3221224448 3221200476 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 110924 110831 162 162 0 110762 0 [pid=30252] vsize: 443696 Current children cumulated CPU time (s) 194.39 Current children cumulated vsize (Kb) 445824 [startup+210.023 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 136823 0 0 0 19866 540 0 0 25 0 1 0 1788484591 474517504 115756 4294967295 134512640 135167914 3221224448 3221200992 134843420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30252/statm): 115849 115756 162 162 0 115687 0 [pid=30252] vsize: 463396 Current children cumulated CPU time (s) 204.07 Current children cumulated vsize (Kb) 465524 [startup+220.024 s] Raw data (loadavg): 0.99 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 141715 0 0 0 20816 563 0 0 25 0 1 0 1788484591 494555136 120648 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 120741 120648 162 162 0 120579 0 [pid=30252] vsize: 482964 Current children cumulated CPU time (s) 213.8 Current children cumulated vsize (Kb) 485092 [startup+230.025 s] Raw data (loadavg): 0.99 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 146413 0 0 0 21761 584 0 0 25 0 1 0 1788484591 513798144 125346 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 125439 125346 162 162 0 125277 0 [pid=30252] vsize: 501756 Current children cumulated CPU time (s) 223.46 Current children cumulated vsize (Kb) 503884 [startup+240.026 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 151365 0 0 0 22703 609 0 0 25 0 1 0 1788484591 534081536 130298 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30252/statm): 130391 130298 162 162 0 130229 0 [pid=30252] vsize: 521564 Current children cumulated CPU time (s) 233.13 Current children cumulated vsize (Kb) 523692 [startup+250.027 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 156201 0 0 0 23648 631 0 0 25 0 1 0 1788484591 553889792 135134 4294967295 134512640 135167914 3221224448 3221201052 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 135227 135134 162 162 0 135065 0 [pid=30252] vsize: 540908 Current children cumulated CPU time (s) 242.8 Current children cumulated vsize (Kb) 543036 [startup+260.028 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 160857 0 0 0 24598 653 0 0 25 0 1 0 1788484591 572960768 139790 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 139883 139790 162 162 0 139721 0 [pid=30252] vsize: 559532 Current children cumulated CPU time (s) 252.52 Current children cumulated vsize (Kb) 561660 [startup+270.028 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 165591 0 0 0 25545 676 0 0 25 0 1 0 1788484591 592351232 144524 4294967295 134512640 135167914 3221224448 3221200448 134845042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30252/statm): 144617 144524 162 162 0 144455 0 [pid=30252] vsize: 578468 Current children cumulated CPU time (s) 262.22 Current children cumulated vsize (Kb) 580596 [startup+280.029 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 187783 0 0 0 26454 739 0 0 25 0 1 0 1788484591 783175680 166716 4294967295 134512640 135167914 3221224448 3221201536 134625368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 191205 166722 162 162 0 191043 0 [pid=30252] vsize: 764820 Current children cumulated CPU time (s) 271.94 Current children cumulated vsize (Kb) 766948 [startup+290.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 212179 0 0 0 27398 796 0 0 25 0 1 0 1788484591 783175680 191112 4294967295 134512640 135167914 3221224448 3221201536 134625428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 191205 191112 162 162 0 191043 0 [pid=30252] vsize: 764820 Current children cumulated CPU time (s) 281.95 Current children cumulated vsize (Kb) 766948 [startup+300.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 214001 0 0 0 28373 808 0 0 25 0 1 0 1788484591 704249856 171843 4294967295 134512640 135167914 3221224448 3221200700 134934490 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 171936 171843 162 162 0 171774 0 [pid=30252] vsize: 687744 Current children cumulated CPU time (s) 291.82 Current children cumulated vsize (Kb) 689872 [startup+310.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 218899 0 0 0 29316 833 0 0 25 0 1 0 1788484591 724312064 176741 4294967295 134512640 135167914 3221224448 3221201296 134695738 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30252/statm): 176834 176741 162 162 0 176672 0 [pid=30252] vsize: 707336 Current children cumulated CPU time (s) 301.5 Current children cumulated vsize (Kb) 709464 [startup+320.033 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 224140 0 0 0 30256 862 0 0 25 0 1 0 1788484591 745779200 181982 4294967295 134512640 135167914 3221224448 3221200172 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/30252/statm): 182075 181982 162 162 0 181913 0 [pid=30252] vsize: 728300 Current children cumulated CPU time (s) 311.19 Current children cumulated vsize (Kb) 730428 [startup+330.035 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 229368 0 0 0 31192 888 0 0 25 0 1 0 1788484591 767193088 187210 4294967295 134512640 135167914 3221224448 3221200640 134619683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30252/statm): 187303 187210 162 162 0 187141 0 [pid=30252] vsize: 749212 Current children cumulated CPU time (s) 320.81 Current children cumulated vsize (Kb) 751340 [startup+340.036 s] Raw data (loadavg): 0.99 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 234443 0 0 0 32133 910 0 0 25 0 1 0 1788484591 787980288 192285 4294967295 134512640 135167914 3221224448 3221200156 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 192378 192285 162 162 0 192216 0 [pid=30252] vsize: 769512 Current children cumulated CPU time (s) 330.44 Current children cumulated vsize (Kb) 771640 [startup+350.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 239562 0 0 0 33076 935 0 0 25 0 1 0 1788484591 808947712 197404 4294967295 134512640 135167914 3221224448 3221200220 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 197497 197404 162 162 0 197335 0 [pid=30252] vsize: 789988 Current children cumulated CPU time (s) 340.12 Current children cumulated vsize (Kb) 792116 [startup+360.037 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 244658 0 0 0 34013 964 0 0 25 0 1 0 1788484591 829820928 202500 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 202593 202500 162 162 0 202431 0 [pid=30252] vsize: 810372 Current children cumulated CPU time (s) 349.78 Current children cumulated vsize (Kb) 812500 [startup+370.037 s] Raw data (loadavg): 0.99 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 249828 0 0 0 34955 989 0 0 25 0 1 0 1788484591 851001344 207670 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 207764 207670 162 162 0 207602 0 [pid=30252] vsize: 831056 Current children cumulated CPU time (s) 359.45 Current children cumulated vsize (Kb) 833184 [startup+380.039 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 254996 0 0 0 35897 1015 0 0 25 0 1 0 1788484591 872165376 212838 4294967295 134512640 135167914 3221224448 3221200348 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 212931 212838 162 162 0 212769 0 [pid=30252] vsize: 851724 Current children cumulated CPU time (s) 369.13 Current children cumulated vsize (Kb) 853852 [startup+390.04 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 260138 0 0 0 36835 1042 0 0 25 0 1 0 1788484591 893227008 217980 4294967295 134512640 135167914 3221224448 3221200704 134849592 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30252/statm): 218073 217980 162 162 0 217911 0 [pid=30252] vsize: 872292 Current children cumulated CPU time (s) 378.78 Current children cumulated vsize (Kb) 874420 [startup+400.041 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 265343 0 0 0 37775 1067 0 0 25 0 1 0 1788484591 914546688 223185 4294967295 134512640 135167914 3221224448 3221201292 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/30252/statm): 223278 223185 162 162 0 223116 0 [pid=30252] vsize: 893112 Current children cumulated CPU time (s) 388.43 Current children cumulated vsize (Kb) 895240 [startup+410.042 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) R 30247 30247 6847 0 -1 0 270456 0 0 0 38713 1094 0 0 25 0 1 0 1788484591 935489536 227818 4294967295 134512640 135167914 3221224448 3221202336 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30252/statm): 228391 227818 162 162 0 228229 0 [pid=30252] vsize: 913564 Current children cumulated CPU time (s) 398.08 Current children cumulated vsize (Kb) 915692 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+412.946 s] Raw data (loadavg): 0.99 0.98 0.91 1/57 30252 Raw data (/proc/30247/stat): 30247 (minisat+_script) S 30246 30247 6847 0 -1 0 314 345 0 0 0 1 0 0 22 0 1 0 1788484584 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30247/statm): 532 234 485 147 0 385 0 [pid=30247] vsize: 2128 Raw data (/proc/30252/stat): 30252 (minisat+_bignum) T 30247 30247 6847 0 -1 0 271933 0 0 0 38986 1100 0 0 25 0 1 0 1788484591 941543424 228785 4294967295 134512640 135167914 3221224448 3221200380 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/30252/statm): 229869 228785 162 162 0 229707 0 [pid=30252] vsize: 919476 Current children cumulated CPU time (s) 400.87 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -30247 Sleeping 2 seconds One traced child (pid=30247) ended because it received signal 15 (SIGTERM) One traced child (pid=30252) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 413.37 CPU time (s): 401.296 CPU user time (s): 389.869 CPU system time (s): 11.4273 CPU usage (%): 97.0791 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !