Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-scsd8.opb |
MD5SUM | 489cca8508801e1a27a21414584e0af6 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 55000 |
Biggest coefficient in the objective function | 216169480454144 |
Number of bits for the biggest coefficient in the objective function | 48 |
Sum of the numbers in the objective function | 581831637603140100 |
Number of bits of the sum of numbers in the objective function | 60 |
Biggest number in a constraint | 216169480454144 |
Number of bits of the biggest number in a constraint | 48 |
Biggest sum of numbers in a constraint | 581831637603140100 |
Number of bits of the biggest sum of numbers | 60 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 55000 |
Total number of constraints | 397 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 397 |
Minimum length of a constraint | 200 |
Maximum length of a constraint | 480 |
LAUNCH ON wulflinc7 THE 2005-09-20 02:53:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3193 boxname=wulflinc7 idbench=849 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 489cca8508801e1a27a21414584e0af6 /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-scsd8.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-scsd8.opb IDLAUNCH: 3193 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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.050 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: 887272 kB Buffers: 11108 kB Cached: 110948 kB SwapCached: 752 kB Active: 35956 kB Inactive: 88684 kB HighTotal: 131008 kB HighFree: 22372 kB LowTotal: 903652 kB LowFree: 864900 kB SwapTotal: 2097136 kB SwapFree: 2095876 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5664 kB Slab: 17056 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:01:05 (client local time) WITH STATUS 0 IN 451.557 SECONDS stats: 3193 7 451.557 0
c Parsing PB file... c PARSE ERROR! [line 2754] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead...
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/9595/stat): 9595 (minisat+_script) R 9594 9595 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796883401 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9595/statm): 174 3 169 147 0 27 0 [pid=9595] 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=9596 New process pid=9597 New process pid=9598 execve syscall for /bin/sed executable One traced child (pid=9597) 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=9598) exited with status: 0 One traced child (pid=9596) exited with status: 0 New process pid=9599 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-scsd8.opb One traced child (pid=9599) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=9600 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-scsd8.opb [startup+10.0038 s] Raw data (loadavg): 0.88 0.97 0.92 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 4265 0 0 0 940 26 0 0 25 0 1 0 1796883408 17809408 4072 4294967295 134512640 135167914 3221224448 3221222640 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 4348 4072 162 162 0 4186 0 [pid=9600] vsize: 17392 Current children cumulated CPU time (s) 9.68 Current children cumulated vsize (Kb) 19520 [startup+20.0044 s] Raw data (loadavg): 0.90 0.97 0.92 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 6613 0 0 0 1905 41 0 0 25 0 1 0 1796883408 27422720 6420 4294967295 134512640 135167914 3221224448 3221221488 134581242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 6695 6420 162 162 0 6533 0 [pid=9600] vsize: 26780 Current children cumulated CPU time (s) 19.48 Current children cumulated vsize (Kb) 28908 [startup+30.005 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 10427 0 0 0 2862 58 0 0 25 0 1 0 1796883408 41025536 9746 4294967295 134512640 135167914 3221224448 3221153340 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 10016 9746 162 162 0 9854 0 [pid=9600] vsize: 40064 Current children cumulated CPU time (s) 29.22 Current children cumulated vsize (Kb) 42192 [startup+40.0057 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 16500 0 0 0 3812 81 0 0 25 0 1 0 1796883408 61849600 14830 4294967295 134512640 135167914 3221224448 3221151996 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 15100 14830 162 162 0 14938 0 [pid=9600] vsize: 60400 Current children cumulated CPU time (s) 38.95 Current children cumulated vsize (Kb) 62528 [startup+50.0073 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 23125 0 0 0 4765 104 0 0 25 0 1 0 1796883408 83587072 20137 4294967295 134512640 135167914 3221224448 3221156784 134849565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 20407 20137 162 162 0 20245 0 [pid=9600] vsize: 81628 Current children cumulated CPU time (s) 48.71 Current children cumulated vsize (Kb) 83756 [startup+60.0079 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 27594 0 0 0 5718 123 0 0 25 0 1 0 1796883408 101892096 24606 4294967295 134512640 135167914 3221224448 3221153280 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 24876 24606 162 162 0 24714 0 [pid=9600] vsize: 99504 Current children cumulated CPU time (s) 58.43 Current children cumulated vsize (Kb) 101632 [startup+70.0076 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 36366 0 0 0 6667 152 0 0 25 0 1 0 1796883408 127021056 30741 4294967295 134512640 135167914 3221224448 3221151548 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 31011 30741 162 162 0 30849 0 [pid=9600] vsize: 124044 Current children cumulated CPU time (s) 68.21 Current children cumulated vsize (Kb) 126172 [startup+80.0092 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 40851 0 0 0 7617 171 0 0 25 0 1 0 1796883408 145391616 35226 4294967295 134512640 135167914 3221224448 3221151644 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 35496 35226 162 162 0 35334 0 [pid=9600] vsize: 141984 Current children cumulated CPU time (s) 77.9 Current children cumulated vsize (Kb) 144112 [startup+90.0098 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 45300 0 0 0 8570 192 0 0 25 0 1 0 1796883408 163614720 39675 4294967295 134512640 135167914 3221224448 3221156092 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 39945 39675 162 162 0 39783 0 [pid=9600] vsize: 159780 Current children cumulated CPU time (s) 87.64 Current children cumulated vsize (Kb) 161908 [startup+100.01 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 49735 0 0 0 9524 212 0 0 25 0 1 0 1796883408 181780480 44110 4294967295 134512640 135167914 3221224448 3221151388 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 44380 44110 162 162 0 44218 0 [pid=9600] vsize: 177520 Current children cumulated CPU time (s) 97.38 Current children cumulated vsize (Kb) 179648 [startup+110.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 62798 0 0 0 10470 250 0 0 25 0 1 0 1796883408 213688320 51900 4294967295 134512640 135167914 3221224448 3221154012 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 52170 51900 162 162 0 52008 0 [pid=9600] vsize: 208680 Current children cumulated CPU time (s) 107.22 Current children cumulated vsize (Kb) 210808 [startup+120.012 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 67291 0 0 0 11420 271 0 0 25 0 1 0 1796883408 232091648 56393 4294967295 134512640 135167914 3221224448 3221151816 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 56663 56393 162 162 0 56501 0 [pid=9600] vsize: 226652 Current children cumulated CPU time (s) 116.93 Current children cumulated vsize (Kb) 228780 [startup+130.012 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 71754 0 0 0 12371 292 0 0 25 0 1 0 1796883408 250372096 60856 4294967295 134512640 135167914 3221224448 3221153852 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 61126 60856 162 162 0 60964 0 [pid=9600] vsize: 244504 Current children cumulated CPU time (s) 126.65 Current children cumulated vsize (Kb) 246632 [startup+140.013 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 76164 0 0 0 13321 313 0 0 25 0 1 0 1796883408 268435456 65266 4294967295 134512640 135167914 3221224448 3221153340 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 65536 65266 162 162 0 65374 0 [pid=9600] vsize: 262144 Current children cumulated CPU time (s) 136.36 Current children cumulated vsize (Kb) 264272 [startup+150.015 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 80586 0 0 0 14275 330 0 0 25 0 1 0 1796883408 286547968 69688 4294967295 134512640 135167914 3221224448 3221151772 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 69958 69688 162 162 0 69796 0 [pid=9600] vsize: 279832 Current children cumulated CPU time (s) 146.07 Current children cumulated vsize (Kb) 281960 [startup+160.015 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 84967 0 0 0 15229 350 0 0 25 0 1 0 1796883408 304492544 74069 4294967295 134512640 135167914 3221224448 3221158064 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 74339 74069 162 162 0 74177 0 [pid=9600] vsize: 297356 Current children cumulated CPU time (s) 155.81 Current children cumulated vsize (Kb) 299484 [startup+170.016 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 89305 0 0 0 16182 369 0 0 25 0 1 0 1796883408 322260992 78407 4294967295 134512640 135167914 3221224448 3221153212 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 78677 78407 162 162 0 78515 0 [pid=9600] vsize: 314708 Current children cumulated CPU time (s) 165.53 Current children cumulated vsize (Kb) 316836 [startup+180.017 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 113788 0 0 0 17098 431 0 0 25 0 1 0 1796883408 422543360 102890 4294967295 134512640 135167914 3221224448 3221154720 134625414 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 103160 102890 162 162 0 102998 0 [pid=9600] vsize: 412640 Current children cumulated CPU time (s) 175.31 Current children cumulated vsize (Kb) 414768 [startup+190.017 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 115301 0 0 0 18080 440 0 0 25 0 1 0 1796883408 385544192 93857 4294967295 134512640 135167914 3221224448 3221153900 134844675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 94127 93857 162 162 0 93965 0 [pid=9600] vsize: 376508 Current children cumulated CPU time (s) 185.22 Current children cumulated vsize (Kb) 378636 [startup+200.018 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 119834 0 0 0 19028 463 0 0 25 0 1 0 1796883408 404111360 98390 4294967295 134512640 135167914 3221224448 3221152932 134619060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 98660 98390 162 162 0 98498 0 [pid=9600] vsize: 394640 Current children cumulated CPU time (s) 194.93 Current children cumulated vsize (Kb) 396768 [startup+210.018 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 124381 0 0 0 19972 488 0 0 25 0 1 0 1796883408 422735872 102937 4294967295 134512640 135167914 3221224448 3221152288 134844650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 103207 102937 162 162 0 103045 0 [pid=9600] vsize: 412828 Current children cumulated CPU time (s) 204.62 Current children cumulated vsize (Kb) 414956 [startup+220.019 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 128847 0 0 0 20922 510 0 0 25 0 1 0 1796883408 441028608 107403 4294967295 134512640 135167914 3221224448 3221157120 134843001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 107673 107403 162 162 0 107511 0 [pid=9600] vsize: 430692 Current children cumulated CPU time (s) 214.34 Current children cumulated vsize (Kb) 432820 [startup+230.02 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 133335 0 0 0 21873 529 0 0 25 0 1 0 1796883408 459411456 111891 4294967295 134512640 135167914 3221224448 3221153436 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 112161 111891 162 162 0 111999 0 [pid=9600] vsize: 448644 Current children cumulated CPU time (s) 224.04 Current children cumulated vsize (Kb) 450772 [startup+240.02 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 137801 0 0 0 22823 551 0 0 25 0 1 0 1796883408 477704192 116357 4294967295 134512640 135167914 3221224448 3221152540 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 116627 116357 162 162 0 116465 0 [pid=9600] vsize: 466508 Current children cumulated CPU time (s) 233.76 Current children cumulated vsize (Kb) 468636 [startup+250.021 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 142281 0 0 0 23771 575 0 0 25 0 1 0 1796883408 496054272 120837 4294967295 134512640 135167914 3221224448 3221151196 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 121107 120837 162 162 0 120945 0 [pid=9600] vsize: 484428 Current children cumulated CPU time (s) 243.48 Current children cumulated vsize (Kb) 486556 [startup+260.022 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 146765 0 0 0 24722 595 0 0 25 0 1 0 1796883408 514420736 125321 4294967295 134512640 135167914 3221224448 3221152672 134843081 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 125591 125321 162 162 0 125429 0 [pid=9600] vsize: 502364 Current children cumulated CPU time (s) 253.19 Current children cumulated vsize (Kb) 504492 [startup+270.021 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 151279 0 0 0 25673 617 0 0 25 0 1 0 1796883408 532910080 129835 4294967295 134512640 135167914 3221224448 3221154176 134624019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 130105 129835 162 162 0 129943 0 [pid=9600] vsize: 520420 Current children cumulated CPU time (s) 262.92 Current children cumulated vsize (Kb) 522548 [startup+280.022 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 155712 0 0 0 26624 638 0 0 25 0 1 0 1796883408 551067648 134268 4294967295 134512640 135167914 3221224448 3221152640 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 134538 134268 162 162 0 134376 0 [pid=9600] vsize: 538152 Current children cumulated CPU time (s) 272.64 Current children cumulated vsize (Kb) 540280 [startup+290.022 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 160141 0 0 0 27577 657 0 0 25 0 1 0 1796883408 569208832 138697 4294967295 134512640 135167914 3221224448 3221151644 134625636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 138967 138697 162 162 0 138805 0 [pid=9600] vsize: 555868 Current children cumulated CPU time (s) 282.36 Current children cumulated vsize (Kb) 557996 [startup+300.023 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 164517 0 0 0 28529 678 0 0 25 0 1 0 1796883408 587132928 143073 4294967295 134512640 135167914 3221224448 3221152688 134693561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 143343 143073 162 162 0 143181 0 [pid=9600] vsize: 573372 Current children cumulated CPU time (s) 292.09 Current children cumulated vsize (Kb) 575500 [startup+310.024 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 168886 0 0 0 29482 698 0 0 25 0 1 0 1796883408 605028352 147442 4294967295 134512640 135167914 3221224448 3221152652 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 147712 147442 162 162 0 147550 0 [pid=9600] vsize: 590848 Current children cumulated CPU time (s) 301.82 Current children cumulated vsize (Kb) 592976 [startup+320.024 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 173264 0 0 0 30435 718 0 0 25 0 1 0 1796883408 622960640 151820 4294967295 134512640 135167914 3221224448 3221151164 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 152090 151820 162 162 0 151928 0 [pid=9600] vsize: 608360 Current children cumulated CPU time (s) 311.55 Current children cumulated vsize (Kb) 610488 [startup+330.026 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 194621 0 0 0 31345 780 0 0 25 0 1 0 1796883408 812605440 173177 4294967295 134512640 135167914 3221224448 3221154720 134625368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 198390 173183 162 162 0 198228 0 [pid=9600] vsize: 793560 Current children cumulated CPU time (s) 321.27 Current children cumulated vsize (Kb) 795688 [startup+340.027 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 219564 0 0 0 32285 840 0 0 25 0 1 0 1796883408 812605440 198120 4294967295 134512640 135167914 3221224448 3221154720 134625423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 198390 198120 162 162 0 198228 0 [pid=9600] vsize: 793560 Current children cumulated CPU time (s) 331.27 Current children cumulated vsize (Kb) 795688 [startup+350.027 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 220827 0 0 0 33265 851 0 0 25 0 1 0 1796883408 731389952 178292 4294967295 134512640 135167914 3221224448 3221154380 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 178562 178292 162 162 0 178400 0 [pid=9600] vsize: 714248 Current children cumulated CPU time (s) 341.18 Current children cumulated vsize (Kb) 716376 [startup+360.028 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 225382 0 0 0 34215 872 0 0 25 0 1 0 1796883408 750047232 182847 4294967295 134512640 135167914 3221224448 3221152284 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 183117 182847 162 162 0 182955 0 [pid=9600] vsize: 732468 Current children cumulated CPU time (s) 350.89 Current children cumulated vsize (Kb) 734596 [startup+370.028 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 229980 0 0 0 35167 893 0 0 25 0 1 0 1796883408 768880640 187445 4294967295 134512640 135167914 3221224448 3221154544 134849560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 187715 187445 162 162 0 187553 0 [pid=9600] vsize: 750860 Current children cumulated CPU time (s) 360.62 Current children cumulated vsize (Kb) 752988 [startup+380.028 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 234552 0 0 0 36119 913 0 0 25 0 1 0 1796883408 787607552 192017 4294967295 134512640 135167914 3221224448 3221151164 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 192287 192017 162 162 0 192125 0 [pid=9600] vsize: 769148 Current children cumulated CPU time (s) 370.34 Current children cumulated vsize (Kb) 771276 [startup+390.028 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 239124 0 0 0 37065 936 0 0 25 0 1 0 1796883408 806334464 196589 4294967295 134512640 135167914 3221224448 3221151164 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 196859 196589 162 162 0 196697 0 [pid=9600] vsize: 787436 Current children cumulated CPU time (s) 380.03 Current children cumulated vsize (Kb) 789564 [startup+400.029 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 243687 0 0 0 38011 959 0 0 25 0 1 0 1796883408 825024512 201152 4294967295 134512640 135167914 3221224448 3221155808 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 201422 201152 162 162 0 201260 0 [pid=9600] vsize: 805688 Current children cumulated CPU time (s) 389.72 Current children cumulated vsize (Kb) 807816 [startup+410.03 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 248216 0 0 0 38962 981 0 0 25 0 1 0 1796883408 843575296 205681 4294967295 134512640 135167914 3221224448 3221152112 134625112 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 205951 205681 162 162 0 205789 0 [pid=9600] vsize: 823804 Current children cumulated CPU time (s) 399.45 Current children cumulated vsize (Kb) 825932 [startup+420.031 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 252725 0 0 0 39909 1004 0 0 25 0 1 0 1796883408 862044160 210190 4294967295 134512640 135167914 3221224448 3221151868 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9600/statm): 210460 210190 162 162 0 210298 0 [pid=9600] vsize: 841840 Current children cumulated CPU time (s) 409.15 Current children cumulated vsize (Kb) 843968 [startup+430.031 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 257288 0 0 0 40861 1025 0 0 25 0 1 0 1796883408 880734208 214753 4294967295 134512640 135167914 3221224448 3221154656 134845442 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 215023 214753 162 162 0 214861 0 [pid=9600] vsize: 860092 Current children cumulated CPU time (s) 418.88 Current children cumulated vsize (Kb) 862220 [startup+440.032 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 261799 0 0 0 41808 1048 0 0 25 0 1 0 1796883408 899211264 219264 4294967295 134512640 135167914 3221224448 3221155380 134619828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9600/statm): 219534 219264 162 162 0 219372 0 [pid=9600] vsize: 878136 Current children cumulated CPU time (s) 428.58 Current children cumulated vsize (Kb) 880264 [startup+450.033 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 266265 0 25 0 42726 1070 0 0 25 0 1 0 1796883408 917086208 222946 4294967295 134512640 135167914 3221224448 3221156972 134620230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 223898 222946 162 162 0 223736 0 [pid=9600] vsize: 895592 Current children cumulated CPU time (s) 437.98 Current children cumulated vsize (Kb) 897720 [startup+460.033 s] Raw data (loadavg): 1.00 0.99 0.93 2/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) R 9595 9595 15400 0 -1 0 270721 0 186 0 43520 1093 0 0 18 0 1 0 1796883408 932483072 225107 4294967295 134512640 135167914 3221224448 3221155548 134693643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9600/statm): 227657 225107 162 162 0 227495 0 [pid=9600] vsize: 910628 Current children cumulated CPU time (s) 446.15 Current children cumulated vsize (Kb) 912756 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+468.815 s] Raw data (loadavg): 1.00 0.99 0.93 1/57 9600 Raw data (/proc/9595/stat): 9595 (minisat+_script) S 9594 9595 15400 0 -1 0 314 332 0 0 0 1 1 0 22 0 1 0 1796883401 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9595/statm): 532 234 485 147 0 385 0 [pid=9595] vsize: 2128 Raw data (/proc/9600/stat): 9600 (minisat+_bignum) T 9595 9595 15400 0 -1 0 273566 0 381 0 44005 1107 0 0 18 0 1 0 1796883408 941543424 222921 4294967295 134512640 135167914 3221224448 3221153884 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/9600/statm): 229869 222921 162 162 0 229707 0 [pid=9600] vsize: 919476 Current children cumulated CPU time (s) 451.14 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -9595 Sleeping 2 seconds One traced child (pid=9595) ended because it received signal 15 (SIGTERM) One traced child (pid=9600) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 469.248 CPU time (s): 451.557 CPU user time (s): 440.054 CPU system time (s): 11.5033 CPU usage (%): 96.2301 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !