Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-adlittle.opb |
MD5SUM | 1bb3cde4ae28db77cb8e051d278e83a5 |
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 | 2460 |
Biggest coefficient in the objective function | 88852135936000 |
Number of bits for the biggest coefficient in the objective function | 47 |
Sum of the numbers in the objective function | 3689448844530141 |
Number of bits of the sum of numbers in the objective function | 52 |
Biggest number in a constraint | 359703511040000 |
Number of bits of the biggest number in a constraint | 49 |
Biggest sum of numbers in a constraint | 6054438712178314 |
Number of bits of the biggest sum of numbers | 53 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2910 |
Total number of constraints | 56 |
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 | 56 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 810 |
LAUNCH ON wulflinc7 THE 2005-09-18 20:09:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2748 boxname=wulflinc7 idbench=404 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1bb3cde4ae28db77cb8e051d278e83a5 /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-adlittle.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-adlittle.opb IDLAUNCH: 2748 /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: 909100 kB Buffers: 35792 kB Cached: 64856 kB SwapCached: 740 kB Active: 69596 kB Inactive: 33684 kB HighTotal: 131008 kB HighFree: 64036 kB LowTotal: 903652 kB LowFree: 845064 kB SwapTotal: 2097136 kB SwapFree: 2095892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 16576 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 20:29:27 (client local time) WITH STATUS 0 IN 1209.97 SECONDS stats: 2748 7 1209.97 0
c Parsing PB file... c PARSE ERROR! [line 101] 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/27543/stat): 27543 (minisat+_script) R 27542 27543 15400 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1785817849 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27543/statm): 174 3 169 147 0 27 0 [pid=27543] 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=27544 New process pid=27545 New process pid=27546 execve syscall for /bin/sed executable One traced child (pid=27545) 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=27546) exited with status: 0 One traced child (pid=27544) exited with status: 0 New process pid=27547 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-20-10-adlittle.opb One traced child (pid=27547) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=27548 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-20-10-adlittle.opb [startup+10.0033 s] Raw data (loadavg): 0.69 0.87 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 432 0 3 0 972 2 0 0 25 0 1 0 1785817856 2162688 421 4294967295 134512640 135167914 3221224448 3221221024 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27548/statm): 528 421 162 162 0 366 0 [pid=27548] vsize: 2112 Current children cumulated CPU time (s) 9.75 Current children cumulated vsize (Kb) 4240 [startup+20.0049 s] Raw data (loadavg): 0.73 0.88 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 432 0 3 0 1972 2 0 0 25 0 1 0 1785817856 2162688 421 4294967295 134512640 135167914 3221224448 3221221644 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27548/statm): 528 421 162 162 0 366 0 [pid=27548] vsize: 2112 Current children cumulated CPU time (s) 19.75 Current children cumulated vsize (Kb) 4240 [startup+30.0056 s] Raw data (loadavg): 0.77 0.88 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 432 0 3 0 2971 2 0 0 25 0 1 0 1785817856 2162688 421 4294967295 134512640 135167914 3221224448 3221221456 134849179 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27548/statm): 528 421 162 162 0 366 0 [pid=27548] vsize: 2112 Current children cumulated CPU time (s) 29.74 Current children cumulated vsize (Kb) 4240 [startup+40.0052 s] Raw data (loadavg): 0.81 0.88 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 648 0 3 0 3971 2 0 0 25 0 1 0 1785817856 2973696 590 4294967295 134512640 135167914 3221224448 3221221992 134694366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27548/statm): 726 590 162 162 0 564 0 [pid=27548] vsize: 2904 Current children cumulated CPU time (s) 39.74 Current children cumulated vsize (Kb) 5032 [startup+50.0068 s] Raw data (loadavg): 0.84 0.89 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 826 0 3 0 4970 3 0 0 25 0 1 0 1785817856 3702784 768 4294967295 134512640 135167914 3221224448 3221202620 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27548/statm): 904 768 162 162 0 742 0 [pid=27548] vsize: 3616 Current children cumulated CPU time (s) 49.74 Current children cumulated vsize (Kb) 5744 [startup+60.0075 s] Raw data (loadavg): 0.86 0.89 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 5970 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221219988 134723216 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 59.74 Current children cumulated vsize (Kb) 5620 [startup+70.0091 s] Raw data (loadavg): 0.88 0.89 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 6970 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221220400 134849068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 69.74 Current children cumulated vsize (Kb) 5620 [startup+80.0097 s] Raw data (loadavg): 0.90 0.90 0.89 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 7970 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221220736 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 79.74 Current children cumulated vsize (Kb) 5620 [startup+90.0094 s] Raw data (loadavg): 0.91 0.90 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 8971 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221220960 134629410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 89.75 Current children cumulated vsize (Kb) 5620 [startup+100.01 s] Raw data (loadavg): 0.93 0.90 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 9971 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221220508 134723265 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 99.75 Current children cumulated vsize (Kb) 5620 [startup+110.011 s] Raw data (loadavg): 0.94 0.90 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 10971 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221221600 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 109.75 Current children cumulated vsize (Kb) 5620 [startup+120.012 s] Raw data (loadavg): 0.95 0.91 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 11971 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221220560 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 119.75 Current children cumulated vsize (Kb) 5620 [startup+130.013 s] Raw data (loadavg): 0.95 0.91 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 12972 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221221184 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 129.76 Current children cumulated vsize (Kb) 5620 [startup+140.013 s] Raw data (loadavg): 0.96 0.91 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 13972 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221221436 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 139.76 Current children cumulated vsize (Kb) 5620 [startup+150.013 s] Raw data (loadavg): 0.97 0.91 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 14972 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221220848 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 149.76 Current children cumulated vsize (Kb) 5620 [startup+160.014 s] Raw data (loadavg): 0.97 0.92 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 15972 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221221056 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 159.76 Current children cumulated vsize (Kb) 5620 [startup+170.014 s] Raw data (loadavg): 0.98 0.92 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 16973 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221221456 134694338 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 169.77 Current children cumulated vsize (Kb) 5620 [startup+180.015 s] Raw data (loadavg): 0.98 0.92 0.90 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 17973 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221222160 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 179.77 Current children cumulated vsize (Kb) 5620 [startup+190.016 s] Raw data (loadavg): 0.98 0.92 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 18973 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221220784 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 189.77 Current children cumulated vsize (Kb) 5620 [startup+200.016 s] Raw data (loadavg): 0.98 0.92 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 19973 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221221612 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 199.77 Current children cumulated vsize (Kb) 5620 [startup+210.017 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 837 0 3 0 20974 3 0 0 25 0 1 0 1785817856 3575808 737 4294967295 134512640 135167914 3221224448 3221221408 134844637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 737 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 209.78 Current children cumulated vsize (Kb) 5620 [startup+220.018 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 847 0 3 0 21974 3 0 0 25 0 1 0 1785817856 3575808 747 4294967295 134512640 135167914 3221224448 3221218736 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 747 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 219.78 Current children cumulated vsize (Kb) 5620 [startup+230.018 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 847 0 3 0 22974 3 0 0 25 0 1 0 1785817856 3575808 747 4294967295 134512640 135167914 3221224448 3221221084 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 747 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 229.78 Current children cumulated vsize (Kb) 5620 [startup+240.018 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 847 0 3 0 23974 3 0 0 25 0 1 0 1785817856 3575808 747 4294967295 134512640 135167914 3221224448 3221222336 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 873 747 162 162 0 711 0 [pid=27548] vsize: 3492 Current children cumulated CPU time (s) 239.78 Current children cumulated vsize (Kb) 5620 [startup+250.018 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 24965 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221218588 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 249.74 Current children cumulated vsize (Kb) 8860 [startup+260.019 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 25965 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219360 134629259 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 259.74 Current children cumulated vsize (Kb) 8860 [startup+270.02 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 26965 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219112 134723211 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 269.74 Current children cumulated vsize (Kb) 8860 [startup+280.02 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 27965 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219264 134696682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 279.74 Current children cumulated vsize (Kb) 8860 [startup+290.021 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 28965 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219600 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 289.74 Current children cumulated vsize (Kb) 8860 [startup+300.022 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 29966 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219504 134694403 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 299.75 Current children cumulated vsize (Kb) 8860 [startup+310.022 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 30966 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219804 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 309.75 Current children cumulated vsize (Kb) 8860 [startup+320.023 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 31966 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219088 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 319.75 Current children cumulated vsize (Kb) 8860 [startup+330.024 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 32966 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219952 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 329.75 Current children cumulated vsize (Kb) 8860 [startup+340.023 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 33966 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219392 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 339.75 Current children cumulated vsize (Kb) 8860 [startup+350.024 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 34967 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219864 134849057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 349.76 Current children cumulated vsize (Kb) 8860 [startup+360.024 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 35967 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219328 134843015 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 359.76 Current children cumulated vsize (Kb) 8860 [startup+370.025 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 36967 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219836 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 369.76 Current children cumulated vsize (Kb) 8860 [startup+380.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 37967 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219360 134630818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 379.76 Current children cumulated vsize (Kb) 8860 [startup+390.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 38967 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219880 134693553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 389.76 Current children cumulated vsize (Kb) 8860 [startup+400.027 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 39968 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220400 134849082 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 399.77 Current children cumulated vsize (Kb) 8860 [startup+410.028 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 40968 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220256 134630908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 409.77 Current children cumulated vsize (Kb) 8860 [startup+420.028 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 41968 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221104 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 419.77 Current children cumulated vsize (Kb) 8860 [startup+430.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 42969 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220336 134843068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 429.78 Current children cumulated vsize (Kb) 8860 [startup+440.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 43969 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219708 134694551 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 439.78 Current children cumulated vsize (Kb) 8860 [startup+450.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 44969 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219856 134849122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 449.78 Current children cumulated vsize (Kb) 8860 [startup+460.03 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 45969 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220596 134630852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 459.78 Current children cumulated vsize (Kb) 8860 [startup+470.03 s] Raw data (loadavg): 1.07 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 46969 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219488 134722521 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 469.78 Current children cumulated vsize (Kb) 8860 [startup+480.031 s] Raw data (loadavg): 1.06 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 47970 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219648 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 479.79 Current children cumulated vsize (Kb) 8860 [startup+490.032 s] Raw data (loadavg): 1.05 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 48970 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220736 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 489.79 Current children cumulated vsize (Kb) 8860 [startup+500.032 s] Raw data (loadavg): 1.04 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 49970 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220768 134628657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 499.79 Current children cumulated vsize (Kb) 8860 [startup+510.033 s] Raw data (loadavg): 1.04 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 50970 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220000 134844637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 509.79 Current children cumulated vsize (Kb) 8860 [startup+520.034 s] Raw data (loadavg): 1.03 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 51971 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219772 134844675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 519.8 Current children cumulated vsize (Kb) 8860 [startup+530.034 s] Raw data (loadavg): 1.03 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 52971 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219984 134843153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 529.8 Current children cumulated vsize (Kb) 8860 [startup+540.034 s] Raw data (loadavg): 1.02 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 53971 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220320 134696745 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 539.8 Current children cumulated vsize (Kb) 8860 [startup+550.034 s] Raw data (loadavg): 1.02 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 54971 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219664 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 549.8 Current children cumulated vsize (Kb) 8860 [startup+560.035 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 55972 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220256 134844708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 559.81 Current children cumulated vsize (Kb) 8860 [startup+570.036 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 56972 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220752 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 569.81 Current children cumulated vsize (Kb) 8860 [startup+580.036 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 57972 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220384 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 579.81 Current children cumulated vsize (Kb) 8860 [startup+590.036 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 58972 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220748 134722660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 589.81 Current children cumulated vsize (Kb) 8860 [startup+600.037 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 59972 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219664 134845937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 599.81 Current children cumulated vsize (Kb) 8860 [startup+610.037 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 60973 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220124 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 609.82 Current children cumulated vsize (Kb) 8860 [startup+620.038 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 61973 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220016 134845937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 619.82 Current children cumulated vsize (Kb) 8860 [startup+630.039 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 62973 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220256 134629161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 629.82 Current children cumulated vsize (Kb) 8860 [startup+640.038 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 63973 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219552 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 639.82 Current children cumulated vsize (Kb) 8860 [startup+650.039 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 64974 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220464 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 649.83 Current children cumulated vsize (Kb) 8860 [startup+660.039 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 65974 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220224 134522299 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 659.83 Current children cumulated vsize (Kb) 8860 [startup+670.041 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 66974 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220880 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 669.83 Current children cumulated vsize (Kb) 8860 [startup+680.042 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 67974 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220020 134845880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 679.83 Current children cumulated vsize (Kb) 8860 [startup+690.041 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 68975 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220432 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 689.84 Current children cumulated vsize (Kb) 8860 [startup+700.042 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 69975 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221200 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 699.84 Current children cumulated vsize (Kb) 8860 [startup+710.043 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 70975 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220080 134844697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 709.84 Current children cumulated vsize (Kb) 8860 [startup+720.043 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 71975 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 719.84 Current children cumulated vsize (Kb) 8860 [startup+730.044 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 72976 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219920 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 729.85 Current children cumulated vsize (Kb) 8860 [startup+740.043 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 73976 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219824 134843030 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 739.85 Current children cumulated vsize (Kb) 8860 [startup+750.044 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 74976 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219872 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 749.85 Current children cumulated vsize (Kb) 8860 [startup+760.044 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 75976 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220304 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 759.85 Current children cumulated vsize (Kb) 8860 [startup+770.045 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 76976 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220536 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 769.85 Current children cumulated vsize (Kb) 8860 [startup+780.046 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 77977 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221104 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 779.86 Current children cumulated vsize (Kb) 8860 [startup+790.047 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 78977 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220400 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 789.86 Current children cumulated vsize (Kb) 8860 [startup+800.047 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 79977 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220672 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 799.86 Current children cumulated vsize (Kb) 8860 [startup+810.048 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 80977 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221052 134844638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 809.86 Current children cumulated vsize (Kb) 8860 [startup+820.049 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 81978 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221100 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 819.87 Current children cumulated vsize (Kb) 8860 [startup+830.049 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 82978 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221472 134629037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 829.87 Current children cumulated vsize (Kb) 8860 [startup+840.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 83978 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219840 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 839.87 Current children cumulated vsize (Kb) 8860 [startup+850.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 84978 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219712 134629345 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 849.87 Current children cumulated vsize (Kb) 8860 [startup+860.051 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 85979 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219184 134629275 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 859.88 Current children cumulated vsize (Kb) 8860 [startup+870.053 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 86979 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219880 134849087 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 869.88 Current children cumulated vsize (Kb) 8860 [startup+880.053 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 87979 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220384 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 879.88 Current children cumulated vsize (Kb) 8860 [startup+890.054 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 88979 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220496 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 889.88 Current children cumulated vsize (Kb) 8860 [startup+900.055 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 89980 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219968 134844718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 899.89 Current children cumulated vsize (Kb) 8860 [startup+910.055 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 90980 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220880 134695269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 909.89 Current children cumulated vsize (Kb) 8860 [startup+920.056 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 91980 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220536 134842997 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 919.89 Current children cumulated vsize (Kb) 8860 [startup+930.057 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 92980 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220712 134844633 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 929.89 Current children cumulated vsize (Kb) 8860 [startup+940.057 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 93981 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220432 134630866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 939.9 Current children cumulated vsize (Kb) 8860 [startup+950.058 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 94981 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220368 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 949.9 Current children cumulated vsize (Kb) 8860 [startup+960.058 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 95981 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219792 134844703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 959.9 Current children cumulated vsize (Kb) 8860 [startup+970.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 96982 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221048 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 969.91 Current children cumulated vsize (Kb) 8860 [startup+980.061 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 97982 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220976 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 979.91 Current children cumulated vsize (Kb) 8860 [startup+990.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 98982 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221440 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 989.91 Current children cumulated vsize (Kb) 8860 [startup+1000.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 99982 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219308 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 999.91 Current children cumulated vsize (Kb) 8860 [startup+1010.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 100982 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219456 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1009.91 Current children cumulated vsize (Kb) 8860 [startup+1020.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 101983 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220320 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1019.92 Current children cumulated vsize (Kb) 8860 [startup+1030.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 102983 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220372 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1029.92 Current children cumulated vsize (Kb) 8860 [startup+1040.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 103983 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219496 134845877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1039.92 Current children cumulated vsize (Kb) 8860 [startup+1050.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 104983 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220908 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1049.92 Current children cumulated vsize (Kb) 8860 [startup+1060.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 105984 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220764 134693585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1059.93 Current children cumulated vsize (Kb) 8860 [startup+1070.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 106984 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220044 134696566 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1069.93 Current children cumulated vsize (Kb) 8860 [startup+1080.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 107984 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220624 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1079.93 Current children cumulated vsize (Kb) 8860 [startup+1090.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 108984 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220592 134630751 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1089.93 Current children cumulated vsize (Kb) 8860 [startup+1100.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 109985 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220416 134629069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1099.94 Current children cumulated vsize (Kb) 8860 [startup+1110.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 110985 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220416 134630795 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1109.94 Current children cumulated vsize (Kb) 8860 [startup+1120.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 111985 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221744 134696578 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1119.94 Current children cumulated vsize (Kb) 8860 [startup+1130.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 112985 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220880 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1129.94 Current children cumulated vsize (Kb) 8860 [startup+1140.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 113986 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220060 134694551 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1139.95 Current children cumulated vsize (Kb) 8860 [startup+1150.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 114986 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221348 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1149.95 Current children cumulated vsize (Kb) 8860 [startup+1160.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 115986 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221376 134696342 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1159.95 Current children cumulated vsize (Kb) 8860 [startup+1170.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 116987 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221221728 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1169.96 Current children cumulated vsize (Kb) 8860 [startup+1180.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 117987 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221219668 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1179.96 Current children cumulated vsize (Kb) 8860 [startup+1190.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 118987 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220008 134849057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1189.96 Current children cumulated vsize (Kb) 8860 [startup+1200.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 119987 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220208 134694489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1199.96 Current children cumulated vsize (Kb) 8860 [startup+1210.08 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 120988 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220272 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1209.97 Current children cumulated vsize (Kb) 8860 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27548 Raw data (/proc/27543/stat): 27543 (minisat+_script) S 27542 27543 15400 0 -1 0 314 332 0 0 0 0 0 1 20 0 1 0 1785817849 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27543/statm): 532 234 485 147 0 385 0 [pid=27543] vsize: 2128 Raw data (/proc/27548/stat): 27548 (minisat+_bignum) R 27543 27543 15400 0 -1 0 1993 0 3 0 120988 8 0 0 25 0 1 0 1785817856 6893568 1561 4294967295 134512640 135167914 3221224448 3221220224 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27548/statm): 1683 1561 162 162 0 1521 0 [pid=27548] vsize: 6732 Current children cumulated CPU time (s) 1209.97 Current children cumulated vsize (Kb) 8860 Sending SIGTERM to -27543 Sleeping 2 seconds One traced child (pid=27543) ended because it received signal 15 (SIGTERM) One traced child (pid=27548) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.08 CPU time (s): 1209.97 CPU user time (s): 1209.88 CPU system time (s): 0.089986 CPU usage (%): 99.9907 Max. virtual memory (cumulated for all children) (Kb): 8860
ERROR: no interpretation found !