Name | mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-net12.opb |
MD5SUM | 1e83ed64f0fd862e44095daf089e38c2 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 863236227986 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 351 |
Biggest coefficient in the objective function | 524288000000 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 1048594922917 |
Number of bits of the sum of numbers in the objective function | 40 |
Biggest number in a constraint | 1075200000000000000 |
Number of bits of the biggest number in a constraint | 60 |
Biggest sum of numbers in a constraint | 2440670651161677657 |
Number of bits of the biggest sum of numbers | 62 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1239.36 |
Number of variables | 653 |
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 | 75 |
LAUNCH ON wulflinc17 THE 2005-09-20 05:39:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3493 boxname=wulflinc17 idbench=1149 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1e83ed64f0fd862e44095daf089e38c2 /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb IDLAUNCH: 3493 /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 : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 897352 kB Buffers: 20508 kB Cached: 88904 kB SwapCached: 612 kB Active: 32152 kB Inactive: 79836 kB HighTotal: 131008 kB HighFree: 42364 kB LowTotal: 903652 kB LowFree: 854988 kB SwapTotal: 2097892 kB SwapFree: 2096676 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5676 kB Slab: 19784 kB Committed_AS: 64316 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:46:28 (client local time) WITH STATUS 0 IN 403.239 SECONDS stats: 3493 7 403.239 0
c Parsing PB file... c PARSE ERROR! [line 653] 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/7595/stat): 7595 (minisat+_script) R 7594 7595 19316 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856109726 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/7595/statm): 174 3 169 147 0 27 0 [pid=7595] 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=7596 New process pid=7597 New process pid=7598 One traced child (pid=7597) exited with status: 0 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 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=7598) exited with status: 0 One traced child (pid=7596) exited with status: 0 New process pid=7599 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb One traced child (pid=7599) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=7600 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb [startup+10.0042 s] Raw data (loadavg): 0.93 0.98 0.98 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 5469 0 0 0 943 23 0 0 25 0 1 0 1856109734 20283392 4835 4294967295 134512640 135167914 3221224448 3221206352 134693566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 4952 4835 162 162 0 4790 0 [pid=7600] vsize: 19808 Current children cumulated CPU time (s) 9.69 Current children cumulated vsize (Kb) 21936 [startup+20.0048 s] Raw data (loadavg): 0.94 0.98 0.98 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 13781 0 0 0 1886 54 0 0 25 0 1 0 1856109734 51630080 12488 4294967295 134512640 135167914 3221224448 3221208240 134625468 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 12605 12488 162 162 0 12443 0 [pid=7600] vsize: 50420 Current children cumulated CPU time (s) 19.43 Current children cumulated vsize (Kb) 52548 [startup+30.0054 s] Raw data (loadavg): 1.02 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 18490 0 0 0 2837 75 0 0 25 0 1 0 1856109734 65519616 15879 4294967295 134512640 135167914 3221224448 3221207152 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 15996 15879 162 162 0 15834 0 [pid=7600] vsize: 63984 Current children cumulated CPU time (s) 29.15 Current children cumulated vsize (Kb) 66112 [startup+40.006 s] Raw data (loadavg): 1.02 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 27447 0 0 0 3787 105 0 0 25 0 1 0 1856109734 91406336 22199 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 22316 22199 162 162 0 22154 0 [pid=7600] vsize: 89264 Current children cumulated CPU time (s) 38.95 Current children cumulated vsize (Kb) 91392 [startup+50.0066 s] Raw data (loadavg): 1.02 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 32334 0 0 0 4737 126 0 0 25 0 1 0 1856109734 111423488 27086 4294967295 134512640 135167914 3221224448 3221207520 134722527 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 27203 27086 162 162 0 27041 0 [pid=7600] vsize: 108812 Current children cumulated CPU time (s) 48.66 Current children cumulated vsize (Kb) 110940 [startup+60.0072 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 37265 0 0 0 5681 149 0 0 25 0 1 0 1856109734 131620864 32017 4294967295 134512640 135167914 3221224448 3221207920 134624972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 32134 32017 162 162 0 31972 0 [pid=7600] vsize: 128536 Current children cumulated CPU time (s) 58.33 Current children cumulated vsize (Kb) 130664 [startup+70.0078 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 42150 0 0 0 6625 172 0 0 25 0 1 0 1856109734 151629824 36902 4294967295 134512640 135167914 3221224448 3221206300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 37019 36902 162 162 0 36857 0 [pid=7600] vsize: 148076 Current children cumulated CPU time (s) 68 Current children cumulated vsize (Kb) 150204 [startup+80.0084 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 55673 0 0 0 7569 211 0 0 25 0 1 0 1856109734 185421824 45152 4294967295 134512640 135167914 3221224448 3221208252 134522320 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 45269 45152 162 162 0 45107 0 [pid=7600] vsize: 181076 Current children cumulated CPU time (s) 77.83 Current children cumulated vsize (Kb) 183204 [startup+90.009 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 60830 0 0 0 8511 234 0 0 25 0 1 0 1856109734 206544896 50309 4294967295 134512640 135167914 3221224448 3221207040 134624821 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 50426 50309 162 162 0 50264 0 [pid=7600] vsize: 201704 Current children cumulated CPU time (s) 87.48 Current children cumulated vsize (Kb) 203832 [startup+100.01 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 65873 0 0 0 9458 258 0 0 25 0 1 0 1856109734 227201024 55352 4294967295 134512640 135167914 3221224448 3221206396 134697040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 55469 55352 162 162 0 55307 0 [pid=7600] vsize: 221876 Current children cumulated CPU time (s) 97.19 Current children cumulated vsize (Kb) 224004 [startup+110.01 s] Raw data (loadavg): 1.00 1.00 0.99 1/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 70903 0 0 0 10405 281 0 0 25 0 1 0 1856109734 247808000 60382 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 60500 60382 162 162 0 60338 0 [pid=7600] vsize: 242000 Current children cumulated CPU time (s) 106.89 Current children cumulated vsize (Kb) 244128 [startup+120.011 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 75911 0 0 0 11349 308 0 0 25 0 1 0 1856109734 268316672 65390 4294967295 134512640 135167914 3221224448 3221206320 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 65507 65390 162 162 0 65345 0 [pid=7600] vsize: 262028 Current children cumulated CPU time (s) 116.6 Current children cumulated vsize (Kb) 264156 [startup+130.011 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 80894 0 0 0 12297 332 0 0 25 0 1 0 1856109734 288727040 70373 4294967295 134512640 135167914 3221224448 3221206432 134694410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 70490 70373 162 162 0 70328 0 [pid=7600] vsize: 281960 Current children cumulated CPU time (s) 126.32 Current children cumulated vsize (Kb) 284088 [startup+140.012 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 106334 0 0 0 13200 402 0 0 25 0 1 0 1856109734 392929280 95813 4294967295 134512640 135167914 3221224448 3221207360 134625423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 95930 95813 162 162 0 95768 0 [pid=7600] vsize: 383720 Current children cumulated CPU time (s) 136.05 Current children cumulated vsize (Kb) 385848 [startup+150.013 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 107955 0 0 0 14180 411 0 0 25 0 1 0 1856109734 356372480 86888 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 87005 86888 162 162 0 86843 0 [pid=7600] vsize: 348020 Current children cumulated CPU time (s) 145.94 Current children cumulated vsize (Kb) 350148 [startup+160.013 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 112991 0 0 0 15126 436 0 0 25 0 1 0 1856109734 376999936 91924 4294967295 134512640 135167914 3221224448 3221207328 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 92041 91924 162 162 0 91879 0 [pid=7600] vsize: 368164 Current children cumulated CPU time (s) 155.65 Current children cumulated vsize (Kb) 370292 [startup+170.014 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 117862 0 0 0 16076 457 0 0 25 0 1 0 1856109734 396951552 96795 4294967295 134512640 135167914 3221224448 3221207104 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7600/statm): 96912 96795 162 162 0 96750 0 [pid=7600] vsize: 387648 Current children cumulated CPU time (s) 165.36 Current children cumulated vsize (Kb) 389776 [startup+180.013 s] Raw data (loadavg): 1.00 1.00 0.99 1/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 122768 0 0 0 17022 479 0 0 25 0 1 0 1856109734 417046528 101701 4294967295 134512640 135167914 3221224448 3221206844 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 101818 101701 162 162 0 101656 0 [pid=7600] vsize: 407272 Current children cumulated CPU time (s) 175.04 Current children cumulated vsize (Kb) 409400 [startup+190.014 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 127638 0 0 0 17969 500 0 0 25 0 1 0 1856109734 436994048 106571 4294967295 134512640 135167914 3221224448 3221206524 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 106688 106571 162 162 0 106526 0 [pid=7600] vsize: 426752 Current children cumulated CPU time (s) 184.72 Current children cumulated vsize (Kb) 428880 [startup+200.014 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 132532 0 0 0 18921 520 0 0 25 0 1 0 1856109734 457039872 111465 4294967295 134512640 135167914 3221224448 3221207136 134847335 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 111582 111465 162 162 0 111420 0 [pid=7600] vsize: 446328 Current children cumulated CPU time (s) 194.44 Current children cumulated vsize (Kb) 448456 [startup+210.014 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 137360 0 0 0 19868 543 0 0 25 0 1 0 1856109734 476815360 116293 4294967295 134512640 135167914 3221224448 3221206204 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 116410 116293 162 162 0 116248 0 [pid=7600] vsize: 465640 Current children cumulated CPU time (s) 204.14 Current children cumulated vsize (Kb) 467768 [startup+220.015 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 142173 0 0 0 20814 567 0 0 25 0 1 0 1856109734 496529408 121106 4294967295 134512640 135167914 3221224448 3221207100 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 121223 121106 162 162 0 121061 0 [pid=7600] vsize: 484892 Current children cumulated CPU time (s) 213.84 Current children cumulated vsize (Kb) 487020 [startup+230.014 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 146727 0 0 0 21766 584 0 0 25 0 1 0 1856109734 515182592 125660 4294967295 134512640 135167914 3221224448 3221206764 134845940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 125777 125660 162 162 0 125615 0 [pid=7600] vsize: 503108 Current children cumulated CPU time (s) 223.53 Current children cumulated vsize (Kb) 505236 [startup+240.015 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 151708 0 0 0 22713 607 0 0 25 0 1 0 1856109734 535584768 130641 4294967295 134512640 135167914 3221224448 3221206256 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 130758 130641 162 162 0 130596 0 [pid=7600] vsize: 523032 Current children cumulated CPU time (s) 233.23 Current children cumulated vsize (Kb) 525160 [startup+250.016 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 156443 0 0 0 23662 628 0 0 25 0 1 0 1856109734 554979328 135376 4294967295 134512640 135167914 3221224448 3221206492 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 135493 135376 162 162 0 135331 0 [pid=7600] vsize: 541972 Current children cumulated CPU time (s) 242.93 Current children cumulated vsize (Kb) 544100 [startup+260.017 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 161025 0 0 0 24615 650 0 0 25 0 1 0 1856109734 573747200 139958 4294967295 134512640 135167914 3221224448 3221206220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 140075 139958 162 162 0 139913 0 [pid=7600] vsize: 560300 Current children cumulated CPU time (s) 252.68 Current children cumulated vsize (Kb) 562428 [startup+270.018 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 165551 0 0 0 25565 672 0 0 25 0 1 0 1856109734 592285696 144484 4294967295 134512640 135167914 3221224448 3221206400 134695619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 144601 144484 162 162 0 144439 0 [pid=7600] vsize: 578404 Current children cumulated CPU time (s) 262.4 Current children cumulated vsize (Kb) 580532 [startup+280.017 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 184881 0 0 0 26483 725 0 0 25 0 1 0 1856109734 782987264 163814 4294967295 134512640 135167914 3221224448 3221206464 134625368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 191159 163821 162 162 0 190997 0 [pid=7600] vsize: 764636 Current children cumulated CPU time (s) 272.11 Current children cumulated vsize (Kb) 766764 [startup+290.018 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 212109 0 0 0 27423 785 0 0 25 0 1 0 1856109734 782987264 191042 4294967295 134512640 135167914 3221224448 3221206448 134625468 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 191159 191042 162 162 0 190997 0 [pid=7600] vsize: 764636 Current children cumulated CPU time (s) 282.11 Current children cumulated vsize (Kb) 766764 [startup+300.019 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 213981 0 0 0 28401 796 0 0 25 0 1 0 1856109734 704266240 171823 4294967295 134512640 135167914 3221224448 3221207808 134621050 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 171940 171823 162 162 0 171778 0 [pid=7600] vsize: 687760 Current children cumulated CPU time (s) 292 Current children cumulated vsize (Kb) 689888 [startup+310.019 s] Raw data (loadavg): 1.00 1.00 0.99 1/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 218803 0 0 0 29351 817 0 0 25 0 1 0 1856109734 724017152 176645 4294967295 134512640 135167914 3221224448 3221206428 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 176762 176645 162 162 0 176600 0 [pid=7600] vsize: 707048 Current children cumulated CPU time (s) 301.71 Current children cumulated vsize (Kb) 709176 [startup+320.02 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 223918 0 0 0 30291 841 0 0 25 0 1 0 1856109734 744968192 181760 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 181877 181760 162 162 0 181715 0 [pid=7600] vsize: 727508 Current children cumulated CPU time (s) 311.35 Current children cumulated vsize (Kb) 729636 [startup+330.02 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 229029 0 0 0 31233 865 0 0 25 0 1 0 1856109734 765906944 186871 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7600/statm): 186989 186871 162 162 0 186827 0 [pid=7600] vsize: 747956 Current children cumulated CPU time (s) 321.01 Current children cumulated vsize (Kb) 750084 [startup+340.021 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 234056 0 0 0 32178 889 0 0 25 0 1 0 1856109734 786493440 191898 4294967295 134512640 135167914 3221224448 3221207528 134845877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 192015 191898 162 162 0 191853 0 [pid=7600] vsize: 768060 Current children cumulated CPU time (s) 330.7 Current children cumulated vsize (Kb) 770188 [startup+350.022 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 239107 0 0 0 33123 914 0 0 25 0 1 0 1856109734 807182336 196949 4294967295 134512640 135167914 3221224448 3221206076 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 197066 196949 162 162 0 196904 0 [pid=7600] vsize: 788264 Current children cumulated CPU time (s) 340.4 Current children cumulated vsize (Kb) 790392 [startup+360.022 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 244151 0 0 0 34067 938 0 0 25 0 1 0 1856109734 827842560 201993 4294967295 134512640 135167914 3221224448 3221206224 134695541 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 202110 201993 162 162 0 201948 0 [pid=7600] vsize: 808440 Current children cumulated CPU time (s) 350.08 Current children cumulated vsize (Kb) 810568 [startup+370.023 s] Raw data (loadavg): 1.07 1.02 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 249263 0 0 0 35009 964 0 0 25 0 1 0 1856109734 848781312 207105 4294967295 134512640 135167914 3221224448 3221206780 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 207222 207105 162 162 0 207060 0 [pid=7600] vsize: 828888 Current children cumulated CPU time (s) 359.76 Current children cumulated vsize (Kb) 831016 [startup+380.022 s] Raw data (loadavg): 1.06 1.02 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 254377 0 0 0 35947 990 0 0 25 0 1 0 1856109734 869728256 212219 4294967295 134512640 135167914 3221224448 3221206220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 212336 212219 162 162 0 212174 0 [pid=7600] vsize: 849344 Current children cumulated CPU time (s) 369.4 Current children cumulated vsize (Kb) 851472 [startup+390.023 s] Raw data (loadavg): 1.05 1.01 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 259454 0 0 0 36895 1014 0 0 25 0 1 0 1856109734 890523648 217296 4294967295 134512640 135167914 3221224448 3221207196 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 217413 217296 162 162 0 217251 0 [pid=7600] vsize: 869652 Current children cumulated CPU time (s) 379.12 Current children cumulated vsize (Kb) 871780 [startup+400.024 s] Raw data (loadavg): 1.04 1.01 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 264573 0 0 0 37834 1038 0 0 25 0 1 0 1856109734 911491072 222415 4294967295 134512640 135167914 3221224448 3221206096 134854320 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7600/statm): 222532 222415 162 162 0 222370 0 [pid=7600] vsize: 890128 Current children cumulated CPU time (s) 388.75 Current children cumulated vsize (Kb) 892256 [startup+410.024 s] Raw data (loadavg): 1.04 1.01 0.99 2/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 269591 0 5 0 38769 1062 0 0 25 0 1 0 1856109734 932016128 225937 4294967295 134512640 135167914 3221224448 3221206172 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 227543 225937 162 162 0 227381 0 [pid=7600] vsize: 910172 Current children cumulated CPU time (s) 398.34 Current children cumulated vsize (Kb) 912300 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+414.719 s] Raw data (loadavg): 1.03 1.01 0.99 1/57 7600 Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/7595/statm): 532 234 485 147 0 385 0 [pid=7595] vsize: 2128 Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 271923 0 9 0 39205 1075 0 0 25 0 1 0 1856109734 941543424 227887 4294967295 134512640 135167914 3221224448 3221206220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7600/statm): 229869 227887 162 162 0 229707 0 [pid=7600] vsize: 919476 Current children cumulated CPU time (s) 402.83 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -7595 Sleeping 2 seconds One traced child (pid=7595) ended because it received signal 15 (SIGTERM) One traced child (pid=7600) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 415.148 CPU time (s): 403.239 CPU user time (s): 392.059 CPU system time (s): 11.1793 CPU usage (%): 97.1312 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !