Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-glass4.opb |
MD5SUM | 5c79ed79e417ba1b9a49f75d042f5e94 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 8257573732279 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 478 |
Biggest coefficient in the objective function | 536870912000000 |
Number of bits for the biggest coefficient in the objective function | 49 |
Sum of the numbers in the objective function | 1073761158741413 |
Number of bits of the sum of numbers in the objective function | 50 |
Biggest number in a constraint | 71583145981965762560 |
Number of bits of the biggest number in a constraint | 66 |
Biggest sum of numbers in a constraint | 303620978593259257856 |
Number of bits of the biggest sum of numbers | 69 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1255.19 |
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 wulflinc22 THE 2005-09-20 02:07:50 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3107 boxname=wulflinc22 idbench=763 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5c79ed79e417ba1b9a49f75d042f5e94 /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb IDLAUNCH: 3107 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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: 889804 kB Buffers: 8104 kB Cached: 109808 kB SwapCached: 476 kB Active: 15576 kB Inactive: 104800 kB HighTotal: 131008 kB HighFree: 21392 kB LowTotal: 903652 kB LowFree: 868412 kB SwapTotal: 2097892 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5676 kB Slab: 18748 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:14:44 (client local time) WITH STATUS 0 IN 400.002 SECONDS stats: 3107 7 400.002 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/15025/stat): 15025 (minisat+_script) R 15024 15025 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854814891 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/15025/statm): 174 3 169 147 0 27 0 [pid=15025] 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=15026 New process pid=15027 New process pid=15028 execve syscall for /bin/sed executable One traced child (pid=15027) 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=15028) exited with status: 0 One traced child (pid=15026) exited with status: 0 New process pid=15029 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb One traced child (pid=15029) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=15030 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb [startup+10.0041 s] Raw data (loadavg): 1.01 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 5174 0 0 0 946 21 0 0 25 0 1 0 1854814897 19070976 4540 4294967295 134512640 135167914 3221224448 3221200860 134694368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 4656 4540 162 162 0 4494 0 [pid=15030] vsize: 18624 Current children cumulated CPU time (s) 9.69 Current children cumulated vsize (Kb) 20752 [startup+20.0048 s] Raw data (loadavg): 1.01 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 13911 0 0 0 1883 54 0 0 25 0 1 0 1854814897 52158464 12618 4294967295 134512640 135167914 3221224448 3221200560 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 12734 12618 162 162 0 12572 0 [pid=15030] vsize: 50936 Current children cumulated CPU time (s) 19.39 Current children cumulated vsize (Kb) 53064 [startup+30.0055 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 18547 0 0 0 2832 75 0 0 25 0 1 0 1854814897 65748992 15936 4294967295 134512640 135167914 3221224448 3221201712 134522355 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 16052 15936 162 162 0 15890 0 [pid=15030] vsize: 64208 Current children cumulated CPU time (s) 29.09 Current children cumulated vsize (Kb) 66336 [startup+40.0062 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 27773 0 0 0 3778 105 0 0 25 0 1 0 1854814897 92737536 22525 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 22641 22525 162 162 0 22479 0 [pid=15030] vsize: 90564 Current children cumulated CPU time (s) 38.85 Current children cumulated vsize (Kb) 92692 [startup+50.0069 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 32445 0 0 0 4727 126 0 0 25 0 1 0 1854814897 111874048 27197 4294967295 134512640 135167914 3221224448 3221204268 134847144 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 27313 27197 162 162 0 27151 0 [pid=15030] vsize: 109252 Current children cumulated CPU time (s) 48.55 Current children cumulated vsize (Kb) 111380 [startup+60.0076 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 37233 0 0 0 5675 147 0 0 25 0 1 0 1854814897 131485696 31985 4294967295 134512640 135167914 3221224448 3221200800 134691325 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 32101 31985 162 162 0 31939 0 [pid=15030] vsize: 128404 Current children cumulated CPU time (s) 58.24 Current children cumulated vsize (Kb) 130532 [startup+70.0083 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 42085 0 0 0 6621 171 0 0 25 0 1 0 1854814897 151359488 36837 4294967295 134512640 135167914 3221224448 3221200756 134622688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 36953 36837 162 162 0 36791 0 [pid=15030] vsize: 147812 Current children cumulated CPU time (s) 67.94 Current children cumulated vsize (Kb) 149940 [startup+80.0091 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 55622 0 0 0 7562 209 0 0 25 0 1 0 1854814897 185208832 45101 4294967295 134512640 135167914 3221224448 3221200396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 45217 45101 162 162 0 45055 0 [pid=15030] vsize: 180868 Current children cumulated CPU time (s) 77.73 Current children cumulated vsize (Kb) 182996 [startup+90.0098 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 60790 0 0 0 8507 235 0 0 25 0 1 0 1854814897 206376960 50269 4294967295 134512640 135167914 3221224448 3221202416 134845895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 50385 50269 162 162 0 50223 0 [pid=15030] vsize: 201540 Current children cumulated CPU time (s) 87.44 Current children cumulated vsize (Kb) 203668 [startup+100.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 65640 0 0 0 9452 258 0 0 25 0 1 0 1854814897 226242560 55119 4294967295 134512640 135167914 3221224448 3221200548 134624735 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 55235 55119 162 162 0 55073 0 [pid=15030] vsize: 220940 Current children cumulated CPU time (s) 97.12 Current children cumulated vsize (Kb) 223068 [startup+110.011 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 70484 0 0 0 10397 282 0 0 25 0 1 0 1854814897 246083584 59963 4294967295 134512640 135167914 3221224448 3221201020 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 60079 59963 162 162 0 59917 0 [pid=15030] vsize: 240316 Current children cumulated CPU time (s) 106.81 Current children cumulated vsize (Kb) 242444 [startup+120.012 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 75352 0 0 0 11345 307 0 0 25 0 1 0 1854814897 266027008 64831 4294967295 134512640 135167914 3221224448 3221200668 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 64948 64831 162 162 0 64786 0 [pid=15030] vsize: 259792 Current children cumulated CPU time (s) 116.54 Current children cumulated vsize (Kb) 261920 [startup+130.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 80154 0 0 0 12293 329 0 0 25 0 1 0 1854814897 285691904 69633 4294967295 134512640 135167914 3221224448 3221201696 134695961 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 69749 69633 162 162 0 69587 0 [pid=15030] vsize: 278996 Current children cumulated CPU time (s) 126.24 Current children cumulated vsize (Kb) 281124 [startup+140.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 84957 0 0 0 13242 348 0 0 25 0 1 0 1854814897 305364992 74436 4294967295 134512640 135167914 3221224448 3221200512 134694389 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 74552 74436 162 162 0 74390 0 [pid=15030] vsize: 298208 Current children cumulated CPU time (s) 135.92 Current children cumulated vsize (Kb) 300336 [startup+150.015 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 106880 0 0 0 14183 401 0 0 25 0 1 0 1854814897 351965184 85813 4294967295 134512640 135167914 3221224448 3221200956 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 85929 85813 162 162 0 85767 0 [pid=15030] vsize: 343716 Current children cumulated CPU time (s) 145.86 Current children cumulated vsize (Kb) 345844 [startup+160.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 112079 0 0 0 15125 427 0 0 25 0 1 0 1854814897 373260288 91012 4294967295 134512640 135167914 3221224448 3221200992 134844700 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 91128 91012 162 162 0 90966 0 [pid=15030] vsize: 364512 Current children cumulated CPU time (s) 155.54 Current children cumulated vsize (Kb) 366640 [startup+170.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 117137 0 0 0 16066 453 0 0 25 0 1 0 1854814897 393977856 96070 4294967295 134512640 135167914 3221224448 3221201072 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 96186 96070 162 162 0 96024 0 [pid=15030] vsize: 384744 Current children cumulated CPU time (s) 165.21 Current children cumulated vsize (Kb) 386872 [startup+180.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 122158 0 0 0 17011 476 0 0 25 0 1 0 1854814897 414543872 101091 4294967295 134512640 135167914 3221224448 3221201664 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 101207 101091 162 162 0 101045 0 [pid=15030] vsize: 404828 Current children cumulated CPU time (s) 174.89 Current children cumulated vsize (Kb) 406956 [startup+190.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 127173 0 0 0 17957 499 0 0 25 0 1 0 1854814897 435085312 106106 4294967295 134512640 135167914 3221224448 3221201952 134843406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 106222 106106 162 162 0 106060 0 [pid=15030] vsize: 424888 Current children cumulated CPU time (s) 184.58 Current children cumulated vsize (Kb) 427016 [startup+200.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 132202 0 0 0 18904 523 0 0 25 0 1 0 1854814897 455684096 111135 4294967295 134512640 135167914 3221224448 3221200832 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 111251 111135 162 162 0 111089 0 [pid=15030] vsize: 445004 Current children cumulated CPU time (s) 194.29 Current children cumulated vsize (Kb) 447132 [startup+210.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 137140 0 0 0 19850 545 0 0 25 0 1 0 1854814897 475910144 116073 4294967295 134512640 135167914 3221224448 3221200552 134693665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 116189 116073 162 162 0 116027 0 [pid=15030] vsize: 464756 Current children cumulated CPU time (s) 203.97 Current children cumulated vsize (Kb) 466884 [startup+220.019 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 142078 0 0 0 20792 569 0 0 25 0 1 0 1854814897 496136192 121011 4294967295 134512640 135167914 3221224448 3221200348 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 121127 121011 162 162 0 120965 0 [pid=15030] vsize: 484508 Current children cumulated CPU time (s) 213.63 Current children cumulated vsize (Kb) 486636 [startup+230.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 146811 0 0 0 21738 592 0 0 25 0 1 0 1854814897 515522560 125744 4294967295 134512640 135167914 3221224448 3221201824 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 125860 125744 162 162 0 125698 0 [pid=15030] vsize: 503440 Current children cumulated CPU time (s) 223.32 Current children cumulated vsize (Kb) 505568 [startup+240.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 151811 0 0 0 22683 615 0 0 25 0 1 0 1854814897 536002560 130744 4294967295 134512640 135167914 3221224448 3221201888 134844703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 130860 130744 162 162 0 130698 0 [pid=15030] vsize: 523440 Current children cumulated CPU time (s) 233 Current children cumulated vsize (Kb) 525568 [startup+250.021 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 156610 0 0 0 23632 635 0 0 25 0 1 0 1854814897 555659264 135543 4294967295 134512640 135167914 3221224448 3221200768 134843015 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 135659 135543 162 162 0 135497 0 [pid=15030] vsize: 542636 Current children cumulated CPU time (s) 242.69 Current children cumulated vsize (Kb) 544764 [startup+260.022 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 161313 0 0 0 24577 658 0 0 25 0 1 0 1854814897 574922752 140246 4294967295 134512640 135167914 3221224448 3221200828 134722218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 140362 140246 162 162 0 140200 0 [pid=15030] vsize: 561448 Current children cumulated CPU time (s) 252.37 Current children cumulated vsize (Kb) 563576 [startup+270.022 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 166041 0 0 0 25524 679 0 0 25 0 1 0 1854814897 594288640 144974 4294967295 134512640 135167914 3221224448 3221200700 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 145090 144974 162 162 0 144928 0 [pid=15030] vsize: 580360 Current children cumulated CPU time (s) 262.05 Current children cumulated vsize (Kb) 582488 [startup+280.022 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 212239 0 0 0 26384 793 0 0 25 0 1 0 1854814897 783515648 191172 4294967295 134512640 135167914 3221224448 3221201536 134625515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 191288 191172 162 162 0 191126 0 [pid=15030] vsize: 765152 Current children cumulated CPU time (s) 271.79 Current children cumulated vsize (Kb) 767280 [startup+290.023 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 212239 0 0 0 27384 793 0 0 25 0 1 0 1854814897 783515648 191172 4294967295 134512640 135167914 3221224448 3221201488 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 191288 191172 162 162 0 191126 0 [pid=15030] vsize: 765152 Current children cumulated CPU time (s) 281.79 Current children cumulated vsize (Kb) 767280 [startup+300.024 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 214616 0 0 0 28354 809 0 0 25 0 1 0 1854814897 706863104 172458 4294967295 134512640 135167914 3221224448 3221200396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 172574 172458 162 162 0 172412 0 [pid=15030] vsize: 690296 Current children cumulated CPU time (s) 291.65 Current children cumulated vsize (Kb) 692424 [startup+310.024 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 219596 0 0 0 29302 830 0 0 25 0 1 0 1854814897 727261184 177438 4294967295 134512640 135167914 3221224448 3221200172 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 177554 177438 162 162 0 177392 0 [pid=15030] vsize: 710216 Current children cumulated CPU time (s) 301.34 Current children cumulated vsize (Kb) 712344 [startup+320.025 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 224832 0 0 0 30248 855 0 0 25 0 1 0 1854814897 748707840 182674 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 182790 182674 162 162 0 182628 0 [pid=15030] vsize: 731160 Current children cumulated CPU time (s) 311.05 Current children cumulated vsize (Kb) 733288 [startup+330.026 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 230047 0 0 0 31193 879 0 0 25 0 1 0 1854814897 770068480 187889 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 188005 187889 162 162 0 187843 0 [pid=15030] vsize: 752020 Current children cumulated CPU time (s) 320.74 Current children cumulated vsize (Kb) 754148 [startup+340.026 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 235147 0 0 0 32134 904 0 0 25 0 1 0 1854814897 790958080 192989 4294967295 134512640 135167914 3221224448 3221200604 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 193105 192989 162 162 0 192943 0 [pid=15030] vsize: 772420 Current children cumulated CPU time (s) 330.4 Current children cumulated vsize (Kb) 774548 [startup+350.026 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 240331 0 0 0 33073 929 0 0 25 0 1 0 1854814897 812191744 198173 4294967295 134512640 135167914 3221224448 3221202012 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 198289 198173 162 162 0 198127 0 [pid=15030] vsize: 793156 Current children cumulated CPU time (s) 340.04 Current children cumulated vsize (Kb) 795284 [startup+360.027 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 245490 0 0 0 34017 952 0 0 25 0 1 0 1854814897 833323008 203332 4294967295 134512640 135167914 3221224448 3221200800 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 203448 203332 162 162 0 203286 0 [pid=15030] vsize: 813792 Current children cumulated CPU time (s) 349.71 Current children cumulated vsize (Kb) 815920 [startup+370.027 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 250727 0 0 0 34958 977 0 0 25 0 1 0 1854814897 854773760 208569 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15030/statm): 208685 208569 162 162 0 208523 0 [pid=15030] vsize: 834740 Current children cumulated CPU time (s) 359.37 Current children cumulated vsize (Kb) 836868 [startup+380.027 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 255968 0 0 0 35901 1003 0 0 25 0 1 0 1854814897 876240896 213810 4294967295 134512640 135167914 3221224448 3221200864 134619044 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15030/statm): 213926 213810 162 162 0 213764 0 [pid=15030] vsize: 855704 Current children cumulated CPU time (s) 369.06 Current children cumulated vsize (Kb) 857832 [startup+390.027 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 261082 0 0 0 36843 1028 0 0 25 0 1 0 1854814897 897187840 218924 4294967295 134512640 135167914 3221224448 3221201480 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 219040 218924 162 162 0 218878 0 [pid=15030] vsize: 876160 Current children cumulated CPU time (s) 378.73 Current children cumulated vsize (Kb) 878288 [startup+400.028 s] Raw data (loadavg): 1.00 0.97 0.91 2/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 266339 0 45 0 37747 1053 0 0 24 0 1 0 1854814897 917487616 222850 4294967295 134512640 135167914 3221224448 3221200448 134845315 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15030/statm): 223996 222850 162 162 0 223834 0 [pid=15030] vsize: 895984 Current children cumulated CPU time (s) 388.02 Current children cumulated vsize (Kb) 898112 [startup+410.029 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) D 15025 15025 21452 0 -1 0 271082 0 93 0 38638 1078 0 0 18 0 1 0 1854814897 936292352 221324 4294967295 134512640 135167914 3221224448 3221203920 134623811 0 0 5 16386 3222515881 0 0 17 0 0 0 Raw data (/proc/15030/statm): 228587 221324 162 162 0 228425 0 [pid=15030] vsize: 914348 Current children cumulated CPU time (s) 397.18 Current children cumulated vsize (Kb) 916476 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+413.521 s] Raw data (loadavg): 1.00 0.97 0.91 1/57 15030 Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15025/statm): 532 234 485 147 0 385 0 [pid=15025] vsize: 2128 Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 272729 0 173 0 38873 1084 0 0 25 0 1 0 1854814897 941543424 222893 4294967295 134512640 135167914 3221224448 3221201788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15030/statm): 229869 222893 162 162 0 229707 0 [pid=15030] vsize: 919476 Current children cumulated CPU time (s) 399.59 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -15025 Sleeping 2 seconds One traced child (pid=15025) ended because it received signal 15 (SIGTERM) One traced child (pid=15030) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 413.986 CPU time (s): 400.002 CPU user time (s): 388.738 CPU system time (s): 11.2643 CPU usage (%): 96.6221 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !