Name | submitted/manquinho/primes-dimacs-cnf/normalized-par32-2.opb |
MD5SUM | 48ed39004ec868a1cad026c865b17eb2 |
Bench Category | optimization, small integers (OPTSMALLINT) |
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 | 6352 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 6352 |
Number of bits of the sum of numbers in the objective function | 13 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 6352 |
Number of bits of the biggest sum of numbers | 13 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 6352 |
Total number of constraints | 13429 |
Number of constraints which are clauses | 13429 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc31 THE 2005-09-18 15:30:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2536 boxname=wulflinc31 idbench=192 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 48ed39004ec868a1cad026c865b17eb2 /oldhome/oroussel/tmp/wulflinc31/normalized-par32-2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-par32-2.opb IDLAUNCH: 2536 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 693352 kB Buffers: 35712 kB Cached: 274508 kB SwapCached: 1016 kB Active: 102588 kB Inactive: 210440 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 693100 kB SwapTotal: 2097892 kB SwapFree: 2096404 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5768 kB Slab: 22536 kB Committed_AS: 64376 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 15:50:15 (client local time) WITH STATUS 0 IN 1200.15 SECONDS stats: 2536 7 1200.15 0
c Parsing PB file... c Converting 13025 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 9776 24386 | 3258 0 0 nan | 0.000 % | c | 101 | 9776 24386 | 3583 101 1054 10.4 | 24.686 % | c | 251 | 9776 24386 | 3942 251 5083 20.3 | 24.685 % | c | 477 | 9776 24386 | 4336 477 7978 16.7 | 24.685 % | c | 815 | 9776 24386 | 4770 815 19982 24.5 | 24.685 % | c | 1322 | 9776 24386 | 5247 1322 33851 25.6 | 24.685 % | c | 2082 | 9776 24386 | 5771 2082 53893 25.9 | 24.685 % | c | 3222 | 9776 24386 | 6348 3222 85157 26.4 | 24.685 % | c | 4930 | 9776 24386 | 6983 4930 135935 27.6 | 24.685 % | c | 7493 | 9776 24386 | 7682 7493 211186 28.2 | 24.685 % | c | 11337 | 9766 24364 | 8450 6645 174908 26.3 | 24.748 % | c | 17104 | 9766 24364 | 9295 7259 205059 28.2 | 24.748 % | c | 25753 | 9766 24364 | 10224 10390 302144 29.1 | 24.748 % | c | 38728 | 9766 24364 | 11247 11443 271075 23.7 | 24.748 % | c | 58190 | 9766 24364 | 12372 11483 266509 23.2 | 24.748 % | c | 87382 | 9766 24364 | 13609 12488 344337 27.6 | 24.748 % | c | 131171 | 9766 24364 | 14970 10333 228609 22.1 | 24.748 % | c | 196855 | 9766 24364 | 16467 9460 209327 22.1 | 24.748 % | c | 295382 | 9766 24364 | 18114 17181 397699 23.1 | 24.748 % | c | 443171 | 9766 24364 | 19925 16694 376985 22.6 | 24.748 % |
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/15138/stat): 15138 (minisat+_script) R 15137 15138 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1842307292 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/15138/statm): 174 3 169 147 0 27 0 [pid=15138] 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=15139 New process pid=15140 New process pid=15141 execve syscall for /bin/sed executable One traced child (pid=15140) 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=15141) exited with status: 0 One traced child (pid=15139) exited with status: 0 New process pid=15142 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-par32-2.opb [startup+10.0047 s] Raw data (loadavg): 0.67 0.88 0.91 2/58 15142 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1316 0 0 0 985 5 0 0 25 0 1 0 1842307297 5627904 1265 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1265 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 9.92 Current children cumulated vsize (Kb) 7620 [startup+20.0056 s] Raw data (loadavg): 0.72 0.89 0.91 2/58 15144 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 1984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223088 134562128 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 19.91 Current children cumulated vsize (Kb) 7620 [startup+30.0066 s] Raw data (loadavg): 0.76 0.89 0.91 2/58 15144 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 2984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 29.91 Current children cumulated vsize (Kb) 7620 [startup+40.0075 s] Raw data (loadavg): 0.80 0.89 0.91 2/58 15144 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 3984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 39.91 Current children cumulated vsize (Kb) 7620 [startup+50.0084 s] Raw data (loadavg): 0.83 0.89 0.91 2/58 15144 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 4984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223040 134557215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 49.91 Current children cumulated vsize (Kb) 7620 [startup+60.0093 s] Raw data (loadavg): 0.85 0.90 0.91 2/58 15144 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 5985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 59.92 Current children cumulated vsize (Kb) 7620 [startup+70.0103 s] Raw data (loadavg): 0.88 0.90 0.91 2/58 15144 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 6985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223072 134562161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 69.92 Current children cumulated vsize (Kb) 7620 [startup+80.0112 s] Raw data (loadavg): 0.89 0.90 0.91 2/58 15146 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 7985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 79.92 Current children cumulated vsize (Kb) 7620 [startup+90.0121 s] Raw data (loadavg): 0.91 0.91 0.91 2/58 15146 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 8985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 89.92 Current children cumulated vsize (Kb) 7620 [startup+100.013 s] Raw data (loadavg): 0.92 0.91 0.91 2/58 15146 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 9986 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223120 134555585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 99.93 Current children cumulated vsize (Kb) 7620 [startup+110.015 s] Raw data (loadavg): 0.93 0.91 0.91 2/58 15146 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 10986 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 109.93 Current children cumulated vsize (Kb) 7620 [startup+120.016 s] Raw data (loadavg): 0.94 0.91 0.91 2/58 15146 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 11986 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 119.93 Current children cumulated vsize (Kb) 7620 [startup+130.016 s] Raw data (loadavg): 0.95 0.92 0.91 2/58 15146 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1324 0 0 0 12986 5 0 0 25 0 1 0 1842307297 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1273 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 129.93 Current children cumulated vsize (Kb) 7620 [startup+140.017 s] Raw data (loadavg): 0.96 0.92 0.91 2/58 15148 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1324 0 0 0 13987 5 0 0 25 0 1 0 1842307297 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1374 1273 145 145 0 1229 0 [pid=15142] vsize: 5496 Current children cumulated CPU time (s) 139.94 Current children cumulated vsize (Kb) 7620 [startup+150.018 s] Raw data (loadavg): 0.97 0.92 0.91 2/58 15148 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1338 0 0 0 14986 6 0 0 25 0 1 0 1842307297 5685248 1287 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1388 1287 145 145 0 1243 0 [pid=15142] vsize: 5552 Current children cumulated CPU time (s) 149.94 Current children cumulated vsize (Kb) 7676 [startup+160.019 s] Raw data (loadavg): 0.97 0.92 0.91 2/58 15148 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1352 0 0 0 15987 6 0 0 25 0 1 0 1842307297 5758976 1301 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1406 1301 145 145 0 1261 0 [pid=15142] vsize: 5624 Current children cumulated CPU time (s) 159.95 Current children cumulated vsize (Kb) 7748 [startup+170.02 s] Raw data (loadavg): 0.97 0.92 0.91 2/58 15148 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1364 0 0 0 16987 6 0 0 25 0 1 0 1842307297 5824512 1313 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15142/statm): 1422 1313 145 145 0 1277 0 [pid=15142] vsize: 5688 Current children cumulated CPU time (s) 169.95 Current children cumulated vsize (Kb) 7812 [startup+180.021 s] Raw data (loadavg): 0.98 0.93 0.91 2/58 15148 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1391 0 0 0 17985 7 0 0 25 0 1 0 1842307297 5935104 1340 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15142/statm): 1449 1340 145 145 0 1304 0 [pid=15142] vsize: 5796 Current children cumulated CPU time (s) 179.94 Current children cumulated vsize (Kb) 7920 [startup+190.022 s] Raw data (loadavg): 0.98 0.93 0.91 2/58 15148 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1400 0 0 0 18984 7 0 0 25 0 1 0 1842307297 6000640 1349 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1465 1349 145 145 0 1320 0 [pid=15142] vsize: 5860 Current children cumulated CPU time (s) 189.93 Current children cumulated vsize (Kb) 7984 [startup+200.023 s] Raw data (loadavg): 0.98 0.93 0.91 2/58 15150 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1405 0 0 0 19984 7 0 0 25 0 1 0 1842307297 6033408 1354 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1473 1354 145 145 0 1328 0 [pid=15142] vsize: 5892 Current children cumulated CPU time (s) 199.93 Current children cumulated vsize (Kb) 8016 [startup+210.024 s] Raw data (loadavg): 0.98 0.93 0.91 2/58 15150 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1405 0 0 0 20985 7 0 0 25 0 1 0 1842307297 6033408 1354 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1473 1354 145 145 0 1328 0 [pid=15142] vsize: 5892 Current children cumulated CPU time (s) 209.94 Current children cumulated vsize (Kb) 8016 [startup+220.025 s] Raw data (loadavg): 0.99 0.93 0.91 2/58 15150 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1410 0 0 0 21985 7 0 0 25 0 1 0 1842307297 6066176 1359 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1481 1359 145 145 0 1336 0 [pid=15142] vsize: 5924 Current children cumulated CPU time (s) 219.94 Current children cumulated vsize (Kb) 8048 [startup+230.026 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 15150 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1412 0 0 0 22985 7 0 0 25 0 1 0 1842307297 6066176 1361 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1481 1361 145 145 0 1336 0 [pid=15142] vsize: 5924 Current children cumulated CPU time (s) 229.94 Current children cumulated vsize (Kb) 8048 [startup+240.027 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 15150 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1412 0 0 0 23985 7 0 0 25 0 1 0 1842307297 6066176 1361 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1481 1361 145 145 0 1336 0 [pid=15142] vsize: 5924 Current children cumulated CPU time (s) 239.94 Current children cumulated vsize (Kb) 8048 [startup+250.028 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 15150 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1417 0 0 0 24986 7 0 0 25 0 1 0 1842307297 6098944 1366 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1489 1366 145 145 0 1344 0 [pid=15142] vsize: 5956 Current children cumulated CPU time (s) 249.95 Current children cumulated vsize (Kb) 8080 [startup+260.029 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 15152 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1417 0 0 0 25986 7 0 0 25 0 1 0 1842307297 6098944 1366 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1489 1366 145 145 0 1344 0 [pid=15142] vsize: 5956 Current children cumulated CPU time (s) 259.95 Current children cumulated vsize (Kb) 8080 [startup+270.03 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 15152 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1439 0 0 0 26986 7 0 0 25 0 1 0 1842307297 6262784 1388 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1529 1388 145 145 0 1384 0 [pid=15142] vsize: 6116 Current children cumulated CPU time (s) 269.95 Current children cumulated vsize (Kb) 8240 [startup+280.03 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 15152 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 27986 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0 [pid=15142] vsize: 6116 Current children cumulated CPU time (s) 279.95 Current children cumulated vsize (Kb) 8240 [startup+290.032 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 15152 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 28986 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0 [pid=15142] vsize: 6116 Current children cumulated CPU time (s) 289.95 Current children cumulated vsize (Kb) 8240 [startup+300.033 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15152 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 29987 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0 [pid=15142] vsize: 6116 Current children cumulated CPU time (s) 299.96 Current children cumulated vsize (Kb) 8240 [startup+310.034 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15152 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 30987 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0 [pid=15142] vsize: 6116 Current children cumulated CPU time (s) 309.96 Current children cumulated vsize (Kb) 8240 [startup+320.035 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15154 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1447 0 0 0 31987 8 0 0 25 0 1 0 1842307297 6295552 1396 4294967295 134512640 135094434 3221224448 3221223104 134556038 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1537 1396 145 145 0 1392 0 [pid=15142] vsize: 6148 Current children cumulated CPU time (s) 319.97 Current children cumulated vsize (Kb) 8272 [startup+330.034 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15154 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1448 0 0 0 32987 8 0 0 25 0 1 0 1842307297 6295552 1397 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1537 1397 145 145 0 1392 0 [pid=15142] vsize: 6148 Current children cumulated CPU time (s) 329.97 Current children cumulated vsize (Kb) 8272 [startup+340.035 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15154 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1454 0 0 0 33988 8 0 0 25 0 1 0 1842307297 6328320 1403 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1545 1403 145 145 0 1400 0 [pid=15142] vsize: 6180 Current children cumulated CPU time (s) 339.98 Current children cumulated vsize (Kb) 8304 [startup+350.036 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15154 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1454 0 0 0 34988 8 0 0 25 0 1 0 1842307297 6328320 1403 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1545 1403 145 145 0 1400 0 [pid=15142] vsize: 6180 Current children cumulated CPU time (s) 349.98 Current children cumulated vsize (Kb) 8304 [startup+360.037 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15154 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 35988 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0 [pid=15142] vsize: 6212 Current children cumulated CPU time (s) 359.98 Current children cumulated vsize (Kb) 8336 [startup+370.038 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15154 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 36988 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0 [pid=15142] vsize: 6212 Current children cumulated CPU time (s) 369.98 Current children cumulated vsize (Kb) 8336 [startup+380.039 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15156 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 37989 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0 [pid=15142] vsize: 6212 Current children cumulated CPU time (s) 379.99 Current children cumulated vsize (Kb) 8336 [startup+390.04 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15156 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 38988 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0 [pid=15142] vsize: 6212 Current children cumulated CPU time (s) 389.98 Current children cumulated vsize (Kb) 8336 [startup+400.041 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 15156 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1486 0 0 0 39988 8 0 0 25 0 1 0 1842307297 6459392 1435 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1577 1435 145 145 0 1432 0 [pid=15142] vsize: 6308 Current children cumulated CPU time (s) 399.98 Current children cumulated vsize (Kb) 8432 [startup+410.043 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15156 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1498 0 0 0 40988 8 0 0 25 0 1 0 1842307297 6516736 1447 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1591 1447 145 145 0 1446 0 [pid=15142] vsize: 6364 Current children cumulated CPU time (s) 409.98 Current children cumulated vsize (Kb) 8488 [startup+420.044 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15156 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1502 0 0 0 41988 8 0 0 25 0 1 0 1842307297 6516736 1451 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1591 1451 145 145 0 1446 0 [pid=15142] vsize: 6364 Current children cumulated CPU time (s) 419.98 Current children cumulated vsize (Kb) 8488 [startup+430.044 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15156 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1502 0 0 0 42988 8 0 0 25 0 1 0 1842307297 6516736 1451 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1591 1451 145 145 0 1446 0 [pid=15142] vsize: 6364 Current children cumulated CPU time (s) 429.98 Current children cumulated vsize (Kb) 8488 [startup+440.045 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15158 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1503 0 0 0 43989 8 0 0 25 0 1 0 1842307297 6516736 1452 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1591 1452 145 145 0 1446 0 [pid=15142] vsize: 6364 Current children cumulated CPU time (s) 439.99 Current children cumulated vsize (Kb) 8488 [startup+450.046 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15158 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1503 0 0 0 44989 8 0 0 25 0 1 0 1842307297 6516736 1452 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1591 1452 145 145 0 1446 0 [pid=15142] vsize: 6364 Current children cumulated CPU time (s) 449.99 Current children cumulated vsize (Kb) 8488 [startup+460.048 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15158 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1510 0 0 0 45989 8 0 0 25 0 1 0 1842307297 6549504 1459 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1599 1459 145 145 0 1454 0 [pid=15142] vsize: 6396 Current children cumulated CPU time (s) 459.99 Current children cumulated vsize (Kb) 8520 [startup+470.048 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15158 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1521 0 0 0 46989 8 0 0 25 0 1 0 1842307297 6647808 1470 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1623 1470 145 145 0 1478 0 [pid=15142] vsize: 6492 Current children cumulated CPU time (s) 469.99 Current children cumulated vsize (Kb) 8616 [startup+480.048 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15158 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1525 0 0 0 47989 8 0 0 25 0 1 0 1842307297 6647808 1474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1623 1474 145 145 0 1478 0 [pid=15142] vsize: 6492 Current children cumulated CPU time (s) 479.99 Current children cumulated vsize (Kb) 8616 [startup+490.049 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15158 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1531 0 0 0 48990 9 0 0 25 0 1 0 1842307297 6680576 1480 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1631 1480 145 145 0 1486 0 [pid=15142] vsize: 6524 Current children cumulated CPU time (s) 490.01 Current children cumulated vsize (Kb) 8648 [startup+500.05 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 15160 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1539 0 0 0 49990 9 0 0 25 0 1 0 1842307297 6713344 1488 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1639 1488 145 145 0 1494 0 [pid=15142] vsize: 6556 Current children cumulated CPU time (s) 500.01 Current children cumulated vsize (Kb) 8680 [startup+510.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15160 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1542 0 0 0 50990 9 0 0 25 0 1 0 1842307297 6778880 1491 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1655 1491 145 145 0 1510 0 [pid=15142] vsize: 6620 Current children cumulated CPU time (s) 510.01 Current children cumulated vsize (Kb) 8744 [startup+520.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15160 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1542 0 0 0 51990 9 0 0 25 0 1 0 1842307297 6778880 1491 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1655 1491 145 145 0 1510 0 [pid=15142] vsize: 6620 Current children cumulated CPU time (s) 520.01 Current children cumulated vsize (Kb) 8744 [startup+530.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15160 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1542 0 0 0 52990 9 0 0 25 0 1 0 1842307297 6778880 1491 4294967295 134512640 135094434 3221224448 3221223040 134551876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1655 1491 145 145 0 1510 0 [pid=15142] vsize: 6620 Current children cumulated CPU time (s) 530.01 Current children cumulated vsize (Kb) 8744 [startup+540.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15160 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1544 0 0 0 53990 9 0 0 25 0 1 0 1842307297 6778880 1493 4294967295 134512640 135094434 3221224448 3221223120 134555437 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1655 1493 145 145 0 1510 0 [pid=15142] vsize: 6620 Current children cumulated CPU time (s) 540.01 Current children cumulated vsize (Kb) 8744 [startup+550.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15160 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1544 0 0 0 54991 9 0 0 25 0 1 0 1842307297 6778880 1493 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1655 1493 145 145 0 1510 0 [pid=15142] vsize: 6620 Current children cumulated CPU time (s) 550.02 Current children cumulated vsize (Kb) 8744 [startup+560.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15162 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1554 0 0 0 55991 9 0 0 25 0 1 0 1842307297 6791168 1503 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1658 1503 145 145 0 1513 0 [pid=15142] vsize: 6632 Current children cumulated CPU time (s) 560.02 Current children cumulated vsize (Kb) 8756 [startup+570.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15162 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1562 0 0 0 56991 9 0 0 25 0 1 0 1842307297 6828032 1511 4294967295 134512640 135094434 3221224448 3221223088 134562041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1667 1511 145 145 0 1522 0 [pid=15142] vsize: 6668 Current children cumulated CPU time (s) 570.02 Current children cumulated vsize (Kb) 8792 [startup+580.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15162 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1587 0 0 0 57990 9 0 0 25 0 1 0 1842307297 6914048 1536 4294967295 134512640 135094434 3221224448 3221223072 134562113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1688 1536 145 145 0 1543 0 [pid=15142] vsize: 6752 Current children cumulated CPU time (s) 580.01 Current children cumulated vsize (Kb) 8876 [startup+590.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15162 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1605 0 0 0 58991 9 0 0 25 0 1 0 1842307297 7016448 1554 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1713 1554 145 145 0 1568 0 [pid=15142] vsize: 6852 Current children cumulated CPU time (s) 590.02 Current children cumulated vsize (Kb) 8976 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15162 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1608 0 0 0 59991 9 0 0 25 0 1 0 1842307297 7016448 1557 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1713 1557 145 145 0 1568 0 [pid=15142] vsize: 6852 Current children cumulated CPU time (s) 600.02 Current children cumulated vsize (Kb) 8976 [startup+610.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15162 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1608 0 0 0 60991 9 0 0 25 0 1 0 1842307297 7016448 1557 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1713 1557 145 145 0 1568 0 [pid=15142] vsize: 6852 Current children cumulated CPU time (s) 610.02 Current children cumulated vsize (Kb) 8976 [startup+620.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15164 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1617 0 0 0 61991 9 0 0 25 0 1 0 1842307297 7081984 1566 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1729 1566 145 145 0 1584 0 [pid=15142] vsize: 6916 Current children cumulated CPU time (s) 620.02 Current children cumulated vsize (Kb) 9040 [startup+630.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15164 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1622 0 0 0 62992 9 0 0 25 0 1 0 1842307297 7114752 1571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1571 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 630.03 Current children cumulated vsize (Kb) 9072 [startup+640.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15164 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1625 0 0 0 63992 9 0 0 25 0 1 0 1842307297 7114752 1574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1574 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 640.03 Current children cumulated vsize (Kb) 9072 [startup+650.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15164 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1625 0 0 0 64992 9 0 0 25 0 1 0 1842307297 7114752 1574 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1574 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 650.03 Current children cumulated vsize (Kb) 9072 [startup+660.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15164 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1625 0 0 0 65992 9 0 0 25 0 1 0 1842307297 7114752 1574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1574 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 660.03 Current children cumulated vsize (Kb) 9072 [startup+670.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15164 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 66993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 670.04 Current children cumulated vsize (Kb) 9072 [startup+680.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15166 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 67993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 680.04 Current children cumulated vsize (Kb) 9072 [startup+690.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15166 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 68993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 690.04 Current children cumulated vsize (Kb) 9072 [startup+700.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15166 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 69993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0 [pid=15142] vsize: 6948 Current children cumulated CPU time (s) 700.04 Current children cumulated vsize (Kb) 9072 [startup+710.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15166 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 70994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 710.05 Current children cumulated vsize (Kb) 9136 [startup+720.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15166 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 71994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 720.05 Current children cumulated vsize (Kb) 9136 [startup+730.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15166 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 72994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 730.05 Current children cumulated vsize (Kb) 9136 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15168 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 73994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 740.05 Current children cumulated vsize (Kb) 9136 [startup+750.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15168 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 74995 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 750.06 Current children cumulated vsize (Kb) 9136 [startup+760.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15168 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1638 0 0 0 75995 9 0 0 25 0 1 0 1842307297 7180288 1587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1587 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 760.06 Current children cumulated vsize (Kb) 9136 [startup+770.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15168 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 76995 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 770.06 Current children cumulated vsize (Kb) 9136 [startup+780.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15168 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 77995 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 780.06 Current children cumulated vsize (Kb) 9136 [startup+790.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15168 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 78995 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 790.06 Current children cumulated vsize (Kb) 9136 [startup+800.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15170 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 79996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 800.07 Current children cumulated vsize (Kb) 9136 [startup+810.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15170 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 80996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 810.07 Current children cumulated vsize (Kb) 9136 [startup+820.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15170 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 81996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 820.07 Current children cumulated vsize (Kb) 9136 [startup+830.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15170 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 82996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 830.07 Current children cumulated vsize (Kb) 9136 [startup+840.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15170 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 83997 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0 [pid=15142] vsize: 7012 Current children cumulated CPU time (s) 840.08 Current children cumulated vsize (Kb) 9136 [startup+850.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15170 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1646 0 0 0 84997 9 0 0 25 0 1 0 1842307297 7213056 1595 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1761 1595 145 145 0 1616 0 [pid=15142] vsize: 7044 Current children cumulated CPU time (s) 850.08 Current children cumulated vsize (Kb) 9168 [startup+860.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15172 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1652 0 0 0 85997 9 0 0 25 0 1 0 1842307297 7245824 1601 4294967295 134512640 135094434 3221224448 3221223120 134556291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1769 1601 145 145 0 1624 0 [pid=15142] vsize: 7076 Current children cumulated CPU time (s) 860.08 Current children cumulated vsize (Kb) 9200 [startup+870.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15172 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1653 0 0 0 86997 9 0 0 25 0 1 0 1842307297 7245824 1602 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1769 1602 145 145 0 1624 0 [pid=15142] vsize: 7076 Current children cumulated CPU time (s) 870.08 Current children cumulated vsize (Kb) 9200 [startup+880.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15172 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1653 0 0 0 87998 9 0 0 25 0 1 0 1842307297 7245824 1602 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1769 1602 145 145 0 1624 0 [pid=15142] vsize: 7076 Current children cumulated CPU time (s) 880.09 Current children cumulated vsize (Kb) 9200 [startup+890.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15172 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1664 0 0 0 88997 10 0 0 25 0 1 0 1842307297 7311360 1613 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15142/statm): 1785 1613 145 145 0 1640 0 [pid=15142] vsize: 7140 Current children cumulated CPU time (s) 890.09 Current children cumulated vsize (Kb) 9264 [startup+900.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15172 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1726 0 0 0 89996 10 0 0 25 0 1 0 1842307297 7548928 1675 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1843 1675 145 145 0 1698 0 [pid=15142] vsize: 7372 Current children cumulated CPU time (s) 900.08 Current children cumulated vsize (Kb) 9496 [startup+910.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15172 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1726 0 0 0 90996 10 0 0 25 0 1 0 1842307297 7548928 1675 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1843 1675 145 145 0 1698 0 [pid=15142] vsize: 7372 Current children cumulated CPU time (s) 910.08 Current children cumulated vsize (Kb) 9496 [startup+920.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15174 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1733 0 0 0 91996 10 0 0 25 0 1 0 1842307297 7577600 1682 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1850 1682 145 145 0 1705 0 [pid=15142] vsize: 7400 Current children cumulated CPU time (s) 920.08 Current children cumulated vsize (Kb) 9524 [startup+930.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15174 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1734 0 0 0 92996 10 0 0 25 0 1 0 1842307297 7577600 1683 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1850 1683 145 145 0 1705 0 [pid=15142] vsize: 7400 Current children cumulated CPU time (s) 930.08 Current children cumulated vsize (Kb) 9524 [startup+940.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15174 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1744 0 0 0 93996 10 0 0 25 0 1 0 1842307297 7639040 1693 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1865 1693 145 145 0 1720 0 [pid=15142] vsize: 7460 Current children cumulated CPU time (s) 940.08 Current children cumulated vsize (Kb) 9584 [startup+950.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15174 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1744 0 0 0 94996 10 0 0 25 0 1 0 1842307297 7639040 1693 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1865 1693 145 145 0 1720 0 [pid=15142] vsize: 7460 Current children cumulated CPU time (s) 950.08 Current children cumulated vsize (Kb) 9584 [startup+960.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15174 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1758 0 0 0 95997 10 0 0 25 0 1 0 1842307297 7704576 1707 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1707 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 960.09 Current children cumulated vsize (Kb) 9648 [startup+970.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15174 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 96997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 970.1 Current children cumulated vsize (Kb) 9648 [startup+980.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15176 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 97997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 980.1 Current children cumulated vsize (Kb) 9648 [startup+990.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15176 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 98997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 990.1 Current children cumulated vsize (Kb) 9648 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15176 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 99997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1000.1 Current children cumulated vsize (Kb) 9648 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15176 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 100998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1010.11 Current children cumulated vsize (Kb) 9648 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15176 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 101998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223136 134554751 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1020.11 Current children cumulated vsize (Kb) 9648 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15176 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 102998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1030.11 Current children cumulated vsize (Kb) 9648 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15178 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 103998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1040.11 Current children cumulated vsize (Kb) 9648 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15178 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 104999 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1050.12 Current children cumulated vsize (Kb) 9648 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15178 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 105999 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1060.12 Current children cumulated vsize (Kb) 9648 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15178 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 106999 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1070.12 Current children cumulated vsize (Kb) 9648 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15178 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 108000 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1080.13 Current children cumulated vsize (Kb) 9648 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15178 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1761 0 0 0 109000 11 0 0 25 0 1 0 1842307297 7704576 1710 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1881 1710 145 145 0 1736 0 [pid=15142] vsize: 7524 Current children cumulated CPU time (s) 1090.13 Current children cumulated vsize (Kb) 9648 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15180 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 110000 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0 [pid=15142] vsize: 7588 Current children cumulated CPU time (s) 1100.13 Current children cumulated vsize (Kb) 9712 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15180 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 111000 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0 [pid=15142] vsize: 7588 Current children cumulated CPU time (s) 1110.13 Current children cumulated vsize (Kb) 9712 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15180 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 112000 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0 [pid=15142] vsize: 7588 Current children cumulated CPU time (s) 1120.13 Current children cumulated vsize (Kb) 9712 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15180 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 113001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0 [pid=15142] vsize: 7588 Current children cumulated CPU time (s) 1130.14 Current children cumulated vsize (Kb) 9712 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15180 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 114001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0 [pid=15142] vsize: 7588 Current children cumulated CPU time (s) 1140.14 Current children cumulated vsize (Kb) 9712 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15180 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 115001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0 [pid=15142] vsize: 7588 Current children cumulated CPU time (s) 1150.14 Current children cumulated vsize (Kb) 9712 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15182 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 116001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0 [pid=15142] vsize: 7588 Current children cumulated CPU time (s) 1160.14 Current children cumulated vsize (Kb) 9712 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15182 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 117002 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0 [pid=15142] vsize: 7652 Current children cumulated CPU time (s) 1170.15 Current children cumulated vsize (Kb) 9776 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15182 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 118002 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0 [pid=15142] vsize: 7652 Current children cumulated CPU time (s) 1180.15 Current children cumulated vsize (Kb) 9776 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15182 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 119002 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0 [pid=15142] vsize: 7652 Current children cumulated CPU time (s) 1190.15 Current children cumulated vsize (Kb) 9776 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15182 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 120003 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0 [pid=15142] vsize: 7652 Current children cumulated CPU time (s) 1200.16 Current children cumulated vsize (Kb) 9776 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 15182 Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15138/statm): 531 226 485 147 0 384 0 [pid=15138] vsize: 2124 Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 120003 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0 [pid=15142] vsize: 7652 Current children cumulated CPU time (s) 1200.16 Current children cumulated vsize (Kb) 9776 Sending SIGTERM to -15138 Sleeping 2 seconds One traced child (pid=15138) ended because it received signal 15 (SIGTERM) One traced child (pid=15142) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.13 CPU time (s): 1200.15 CPU user time (s): 1200.03 CPU system time (s): 0.119981 CPU usage (%): 100.002 Max. virtual memory (cumulated for all children) (Kb): 9776
ERROR: no interpretation found !