Name | submitted/manquinho/primes-dimacs-cnf/normalized-f2000.opb |
MD5SUM | 4675a5d50c7e04c9a0597ae768da1a88 |
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 | 4000 |
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 | 4000 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 4000 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 4000 |
Total number of constraints | 10500 |
Number of constraints which are clauses | 10500 |
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 | 2 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc31 THE 2005-09-18 15:08:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2467 boxname=wulflinc31 idbench=123 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4675a5d50c7e04c9a0597ae768da1a88 /oldhome/oroussel/tmp/wulflinc31/normalized-f2000.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-f2000.opb IDLAUNCH: 2467 /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: 693576 kB Buffers: 35624 kB Cached: 274324 kB SwapCached: 1016 kB Active: 102388 kB Inactive: 210380 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 693324 kB SwapTotal: 2097892 kB SwapFree: 2096404 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5768 kB Slab: 22580 kB Committed_AS: 64340 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 15:29:07 (client local time) WITH STATUS 0 IN 1209.83 SECONDS stats: 2467 7 1209.83 0
c Parsing PB file... c Converting 10500 PB-constraints to clauses... c -- Unit propagations: (none) 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 | 10500 29500 | 3500 0 0 nan | 0.000 % | c | 101 | 10500 29500 | 3850 101 5214 51.6 | 0.000 % | c | 254 | 10500 29500 | 4235 254 16768 66.0 | 0.000 % | c | 480 | 10500 29500 | 4658 480 31254 65.1 | 0.000 % | c | 818 | 10500 29500 | 5124 818 54667 66.8 | 0.000 % | c | 1325 | 10500 29500 | 5636 1325 91945 69.4 | 0.000 % | c | 2085 | 10500 29500 | 6200 2085 147368 70.7 | 0.000 % | c | 3224 | 10500 29500 | 6820 3224 227442 70.5 | 0.000 % | c | 4933 | 10500 29500 | 7502 4933 356310 72.2 | 0.000 % | c | 7498 | 10500 29500 | 8252 7498 558986 74.6 | 0.000 % | c | 11342 | 10500 29500 | 9078 7035 532667 75.7 | 0.000 % | c | 17110 | 10500 29500 | 9985 8082 628618 77.8 | 0.000 % | c | 25760 | 10500 29500 | 10984 6399 501007 78.3 | 0.000 % | c | 38734 | 10500 29500 | 12082 8099 680844 84.1 | 0.000 % | c | 58195 | 10500 29500 | 13291 8833 695144 78.7 | 0.000 % | c | 87387 | 10500 29500 | 14620 10633 872256 82.0 | 0.000 % | c | 131179 | 10500 29500 | 16082 9098 714655 78.6 | 0.000 % | c | 196863 | 10500 29500 | 17690 8808 654716 74.3 | 0.000 % | c | 295391 | 10500 29500 | 19459 16874 1288385 76.4 | 0.000 % | c | 443181 | 10500 29500 | 21405 15399 1144903 74.3 | 0.000 % | c | 664864 | 10500 29500 | 23546 18740 1450858 77.4 | 0.000 % |
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/14295/stat): 14295 (minisat+_script) R 14294 14295 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842179474 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14295/statm): 174 3 169 147 0 27 0 [pid=14295] 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=14296 New process pid=14297 New process pid=14298 execve syscall for /bin/sed executable One traced child (pid=14297) 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=14298) exited with status: 0 One traced child (pid=14296) exited with status: 0 New process pid=14299 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-f2000.opb [startup+10.0042 s] Raw data (loadavg): 0.59 0.86 0.94 2/58 14299 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1238 0 0 0 983 6 0 0 25 0 1 0 1842179479 5390336 1225 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 1316 1225 145 145 0 1171 0 [pid=14299] vsize: 5264 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 7388 [startup+20.0051 s] Raw data (loadavg): 0.65 0.86 0.94 2/58 14299 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1495 0 0 0 1978 9 0 0 25 0 1 0 1842179479 6434816 1482 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 1571 1482 145 145 0 1426 0 [pid=14299] vsize: 6284 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 8408 [startup+30.0061 s] Raw data (loadavg): 0.71 0.87 0.94 2/58 14301 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1660 0 0 0 2975 10 0 0 25 0 1 0 1842179479 7106560 1647 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 1735 1647 145 145 0 1590 0 [pid=14299] vsize: 6940 Current children cumulated CPU time (s) 29.85 Current children cumulated vsize (Kb) 9064 [startup+40.007 s] Raw data (loadavg): 0.75 0.87 0.94 2/58 14301 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1748 0 0 0 3973 11 0 0 25 0 1 0 1842179479 7471104 1735 4294967295 134512640 135094434 3221224448 3221223088 134562095 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 1824 1735 145 145 0 1679 0 [pid=14299] vsize: 7296 Current children cumulated CPU time (s) 39.84 Current children cumulated vsize (Kb) 9420 [startup+50.009 s] Raw data (loadavg): 0.79 0.87 0.94 2/58 14301 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1835 0 0 0 4970 13 0 0 25 0 1 0 1842179479 7823360 1822 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 1910 1822 145 145 0 1765 0 [pid=14299] vsize: 7640 Current children cumulated CPU time (s) 49.83 Current children cumulated vsize (Kb) 9764 [startup+60.0109 s] Raw data (loadavg): 0.82 0.88 0.94 2/58 14301 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1875 0 0 0 5970 13 0 0 25 0 1 0 1842179479 7995392 1862 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 1952 1862 145 145 0 1807 0 [pid=14299] vsize: 7808 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 9932 [startup+70.0118 s] Raw data (loadavg): 0.85 0.88 0.94 2/58 14301 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1985 0 0 0 6967 14 0 0 25 0 1 0 1842179479 8441856 1972 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2061 1972 145 145 0 1916 0 [pid=14299] vsize: 8244 Current children cumulated CPU time (s) 69.81 Current children cumulated vsize (Kb) 10368 [startup+80.0127 s] Raw data (loadavg): 0.87 0.89 0.94 2/58 14301 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2052 0 0 0 7965 16 0 0 25 0 1 0 1842179479 8716288 2039 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2128 2039 145 145 0 1983 0 [pid=14299] vsize: 8512 Current children cumulated CPU time (s) 79.81 Current children cumulated vsize (Kb) 10636 [startup+90.0147 s] Raw data (loadavg): 0.89 0.89 0.94 2/58 14303 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2132 0 0 0 8962 17 0 0 25 0 1 0 1842179479 9043968 2119 4294967295 134512640 135094434 3221224448 3221223104 134558033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2208 2119 145 145 0 2063 0 [pid=14299] vsize: 8832 Current children cumulated CPU time (s) 89.79 Current children cumulated vsize (Kb) 10956 [startup+100.016 s] Raw data (loadavg): 0.91 0.89 0.94 2/58 14303 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2145 0 0 0 9961 19 0 0 25 0 1 0 1842179479 9097216 2132 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2221 2132 145 145 0 2076 0 [pid=14299] vsize: 8884 Current children cumulated CPU time (s) 99.8 Current children cumulated vsize (Kb) 11008 [startup+110.018 s] Raw data (loadavg): 0.92 0.89 0.94 2/58 14303 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2254 0 0 0 10958 20 0 0 25 0 1 0 1842179479 9535488 2241 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2328 2241 145 145 0 2183 0 [pid=14299] vsize: 9312 Current children cumulated CPU time (s) 109.78 Current children cumulated vsize (Kb) 11436 [startup+120.019 s] Raw data (loadavg): 0.93 0.90 0.94 2/58 14303 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2280 0 0 0 11957 21 0 0 25 0 1 0 1842179479 9650176 2267 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2356 2267 145 145 0 2211 0 [pid=14299] vsize: 9424 Current children cumulated CPU time (s) 119.78 Current children cumulated vsize (Kb) 11548 [startup+130.02 s] Raw data (loadavg): 0.94 0.90 0.94 2/58 14303 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2317 0 0 0 12956 22 0 0 25 0 1 0 1842179479 9801728 2304 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2393 2304 145 145 0 2248 0 [pid=14299] vsize: 9572 Current children cumulated CPU time (s) 129.78 Current children cumulated vsize (Kb) 11696 [startup+140.022 s] Raw data (loadavg): 0.95 0.90 0.94 2/58 14303 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2317 0 0 0 13956 23 0 0 25 0 1 0 1842179479 9801728 2304 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2393 2304 145 145 0 2248 0 [pid=14299] vsize: 9572 Current children cumulated CPU time (s) 139.79 Current children cumulated vsize (Kb) 11696 [startup+150.023 s] Raw data (loadavg): 0.96 0.91 0.94 2/58 14305 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2327 0 0 0 14955 23 0 0 25 0 1 0 1842179479 9846784 2314 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2404 2314 145 145 0 2259 0 [pid=14299] vsize: 9616 Current children cumulated CPU time (s) 149.78 Current children cumulated vsize (Kb) 11740 [startup+160.024 s] Raw data (loadavg): 0.96 0.91 0.94 2/58 14305 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2349 0 0 0 15954 24 0 0 25 0 1 0 1842179479 9936896 2336 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2426 2336 145 145 0 2281 0 [pid=14299] vsize: 9704 Current children cumulated CPU time (s) 159.78 Current children cumulated vsize (Kb) 11828 [startup+170.025 s] Raw data (loadavg): 0.97 0.91 0.94 2/58 14305 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2367 0 0 0 16954 25 0 0 25 0 1 0 1842179479 10010624 2354 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2444 2354 145 145 0 2299 0 [pid=14299] vsize: 9776 Current children cumulated CPU time (s) 169.79 Current children cumulated vsize (Kb) 11900 [startup+180.026 s] Raw data (loadavg): 0.97 0.91 0.94 2/58 14305 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2481 0 0 0 17952 25 0 0 25 0 1 0 1842179479 10539008 2468 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2573 2468 145 145 0 2428 0 [pid=14299] vsize: 10292 Current children cumulated CPU time (s) 179.77 Current children cumulated vsize (Kb) 12416 [startup+190.028 s] Raw data (loadavg): 0.98 0.92 0.94 2/58 14305 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2481 0 0 0 18952 25 0 0 25 0 1 0 1842179479 10539008 2468 4294967295 134512640 135094434 3221224448 3221223040 134557263 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2573 2468 145 145 0 2428 0 [pid=14299] vsize: 10292 Current children cumulated CPU time (s) 189.77 Current children cumulated vsize (Kb) 12416 [startup+200.029 s] Raw data (loadavg): 0.98 0.92 0.94 2/58 14305 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2486 0 0 0 19951 26 0 0 25 0 1 0 1842179479 10559488 2473 4294967295 134512640 135094434 3221224448 3221223120 134555967 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2578 2473 145 145 0 2433 0 [pid=14299] vsize: 10312 Current children cumulated CPU time (s) 199.77 Current children cumulated vsize (Kb) 12436 [startup+210.031 s] Raw data (loadavg): 0.98 0.92 0.94 2/58 14307 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2501 0 0 0 20950 27 0 0 25 0 1 0 1842179479 10620928 2488 4294967295 134512640 135094434 3221224448 3221223072 134562139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2593 2488 145 145 0 2448 0 [pid=14299] vsize: 10372 Current children cumulated CPU time (s) 209.77 Current children cumulated vsize (Kb) 12496 [startup+220.033 s] Raw data (loadavg): 0.98 0.92 0.94 2/58 14307 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2507 0 0 0 21950 28 0 0 25 0 1 0 1842179479 10645504 2494 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 2599 2494 145 145 0 2454 0 [pid=14299] vsize: 10396 Current children cumulated CPU time (s) 219.78 Current children cumulated vsize (Kb) 12520 [startup+230.034 s] Raw data (loadavg): 0.99 0.92 0.94 2/58 14307 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2547 0 0 0 22949 28 0 0 25 0 1 0 1842179479 10825728 2534 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2643 2534 145 145 0 2498 0 [pid=14299] vsize: 10572 Current children cumulated CPU time (s) 229.77 Current children cumulated vsize (Kb) 12696 [startup+240.035 s] Raw data (loadavg): 0.99 0.93 0.94 2/58 14307 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2551 0 0 0 23949 28 0 0 25 0 1 0 1842179479 10842112 2538 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2647 2538 145 145 0 2502 0 [pid=14299] vsize: 10588 Current children cumulated CPU time (s) 239.77 Current children cumulated vsize (Kb) 12712 [startup+250.035 s] Raw data (loadavg): 0.99 0.93 0.94 2/58 14307 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2551 0 0 0 24949 28 0 0 25 0 1 0 1842179479 10842112 2538 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2647 2538 145 145 0 2502 0 [pid=14299] vsize: 10588 Current children cumulated CPU time (s) 249.77 Current children cumulated vsize (Kb) 12712 [startup+260.037 s] Raw data (loadavg): 0.99 0.93 0.94 2/58 14307 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2589 0 0 0 25949 29 0 0 25 0 1 0 1842179479 10993664 2576 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2684 2576 145 145 0 2539 0 [pid=14299] vsize: 10736 Current children cumulated CPU time (s) 259.78 Current children cumulated vsize (Kb) 12860 [startup+270.038 s] Raw data (loadavg): 0.99 0.93 0.94 2/58 14309 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2694 0 0 0 26947 29 0 0 25 0 1 0 1842179479 11415552 2681 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2787 2681 145 145 0 2642 0 [pid=14299] vsize: 11148 Current children cumulated CPU time (s) 269.76 Current children cumulated vsize (Kb) 13272 [startup+280.038 s] Raw data (loadavg): 0.99 0.93 0.94 2/58 14309 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2694 0 0 0 27947 29 0 0 25 0 1 0 1842179479 11415552 2681 4294967295 134512640 135094434 3221224448 3221223040 134557348 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2787 2681 145 145 0 2642 0 [pid=14299] vsize: 11148 Current children cumulated CPU time (s) 279.76 Current children cumulated vsize (Kb) 13272 [startup+290.04 s] Raw data (loadavg): 0.99 0.94 0.94 2/58 14309 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2755 0 0 0 28947 29 0 0 25 0 1 0 1842179479 11665408 2742 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2848 2742 145 145 0 2703 0 [pid=14299] vsize: 11392 Current children cumulated CPU time (s) 289.76 Current children cumulated vsize (Kb) 13516 [startup+300.041 s] Raw data (loadavg): 0.99 0.94 0.94 2/58 14309 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2793 0 0 0 29947 30 0 0 25 0 1 0 1842179479 11829248 2780 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2888 2780 145 145 0 2743 0 [pid=14299] vsize: 11552 Current children cumulated CPU time (s) 299.77 Current children cumulated vsize (Kb) 13676 [startup+310.042 s] Raw data (loadavg): 0.99 0.94 0.94 2/58 14309 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2806 0 0 0 30947 30 0 0 25 0 1 0 1842179479 11890688 2793 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2903 2793 145 145 0 2758 0 [pid=14299] vsize: 11612 Current children cumulated CPU time (s) 309.77 Current children cumulated vsize (Kb) 13736 [startup+320.043 s] Raw data (loadavg): 0.99 0.94 0.94 2/58 14309 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2813 0 0 0 31947 30 0 0 25 0 1 0 1842179479 11923456 2800 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2911 2800 145 145 0 2766 0 [pid=14299] vsize: 11644 Current children cumulated CPU time (s) 319.77 Current children cumulated vsize (Kb) 13768 [startup+330.044 s] Raw data (loadavg): 0.99 0.94 0.94 2/58 14311 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2813 0 0 0 32947 30 0 0 25 0 1 0 1842179479 11923456 2800 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2911 2800 145 145 0 2766 0 [pid=14299] vsize: 11644 Current children cumulated CPU time (s) 329.77 Current children cumulated vsize (Kb) 13768 [startup+340.045 s] Raw data (loadavg): 0.99 0.94 0.94 2/58 14311 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2813 0 0 0 33947 30 0 0 25 0 1 0 1842179479 11923456 2800 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2911 2800 145 145 0 2766 0 [pid=14299] vsize: 11644 Current children cumulated CPU time (s) 339.77 Current children cumulated vsize (Kb) 13768 [startup+350.046 s] Raw data (loadavg): 0.99 0.94 0.94 2/58 14311 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2820 0 0 0 34947 30 0 0 25 0 1 0 1842179479 11952128 2807 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2918 2807 145 145 0 2773 0 [pid=14299] vsize: 11672 Current children cumulated CPU time (s) 349.77 Current children cumulated vsize (Kb) 13796 [startup+360.048 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14311 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2848 0 0 0 35947 30 0 0 25 0 1 0 1842179479 12083200 2835 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2950 2835 145 145 0 2805 0 [pid=14299] vsize: 11800 Current children cumulated CPU time (s) 359.77 Current children cumulated vsize (Kb) 13924 [startup+370.049 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14311 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2848 0 0 0 36947 31 0 0 25 0 1 0 1842179479 12083200 2835 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2950 2835 145 145 0 2805 0 [pid=14299] vsize: 11800 Current children cumulated CPU time (s) 369.78 Current children cumulated vsize (Kb) 13924 [startup+380.05 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14311 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2848 0 0 0 37948 31 0 0 25 0 1 0 1842179479 12083200 2835 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2950 2835 145 145 0 2805 0 [pid=14299] vsize: 11800 Current children cumulated CPU time (s) 379.79 Current children cumulated vsize (Kb) 13924 [startup+390.05 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14313 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2885 0 0 0 38947 31 0 0 25 0 1 0 1842179479 12234752 2872 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 2987 2872 145 145 0 2842 0 [pid=14299] vsize: 11948 Current children cumulated CPU time (s) 389.78 Current children cumulated vsize (Kb) 14072 [startup+400.051 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14313 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2936 0 0 0 39946 31 0 0 25 0 1 0 1842179479 12443648 2923 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 3038 2923 145 145 0 2893 0 [pid=14299] vsize: 12152 Current children cumulated CPU time (s) 399.77 Current children cumulated vsize (Kb) 14276 [startup+410.053 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14313 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3011 0 0 0 40944 32 0 0 25 0 1 0 1842179479 12746752 2998 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3112 2998 145 145 0 2967 0 [pid=14299] vsize: 12448 Current children cumulated CPU time (s) 409.76 Current children cumulated vsize (Kb) 14572 [startup+420.054 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14313 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3014 0 0 0 41944 32 0 0 25 0 1 0 1842179479 12759040 3001 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3115 3001 145 145 0 2970 0 [pid=14299] vsize: 12460 Current children cumulated CPU time (s) 419.76 Current children cumulated vsize (Kb) 14584 [startup+430.055 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14313 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3039 0 0 0 42944 33 0 0 25 0 1 0 1842179479 12869632 3026 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3142 3026 145 145 0 2997 0 [pid=14299] vsize: 12568 Current children cumulated CPU time (s) 429.77 Current children cumulated vsize (Kb) 14692 [startup+440.056 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14313 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3048 0 0 0 43944 33 0 0 25 0 1 0 1842179479 12910592 3035 4294967295 134512640 135094434 3221224448 3221223120 134555771 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3152 3035 145 145 0 3007 0 [pid=14299] vsize: 12608 Current children cumulated CPU time (s) 439.77 Current children cumulated vsize (Kb) 14732 [startup+450.057 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14315 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3060 0 0 0 44944 33 0 0 25 0 1 0 1842179479 12955648 3047 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3163 3047 145 145 0 3018 0 [pid=14299] vsize: 12652 Current children cumulated CPU time (s) 449.77 Current children cumulated vsize (Kb) 14776 [startup+460.059 s] Raw data (loadavg): 0.99 0.95 0.94 2/58 14315 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3089 0 0 0 45943 33 0 0 25 0 1 0 1842179479 13074432 3076 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3192 3076 145 145 0 3047 0 [pid=14299] vsize: 12768 Current children cumulated CPU time (s) 459.76 Current children cumulated vsize (Kb) 14892 [startup+470.06 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14315 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3093 0 0 0 46943 33 0 0 25 0 1 0 1842179479 13090816 3080 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3196 3080 145 145 0 3051 0 [pid=14299] vsize: 12784 Current children cumulated CPU time (s) 469.76 Current children cumulated vsize (Kb) 14908 [startup+480.061 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14315 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3098 0 0 0 47944 33 0 0 25 0 1 0 1842179479 13111296 3085 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3201 3085 145 145 0 3056 0 [pid=14299] vsize: 12804 Current children cumulated CPU time (s) 479.77 Current children cumulated vsize (Kb) 14928 [startup+490.062 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14315 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3115 0 0 0 48943 33 0 0 25 0 1 0 1842179479 13197312 3102 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3222 3102 145 145 0 3077 0 [pid=14299] vsize: 12888 Current children cumulated CPU time (s) 489.76 Current children cumulated vsize (Kb) 15012 [startup+500.063 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14315 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3123 0 0 0 49944 34 0 0 25 0 1 0 1842179479 13230080 3110 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3230 3110 145 145 0 3085 0 [pid=14299] vsize: 12920 Current children cumulated CPU time (s) 499.78 Current children cumulated vsize (Kb) 15044 [startup+510.064 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14317 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3123 0 0 0 50944 34 0 0 25 0 1 0 1842179479 13230080 3110 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3230 3110 145 145 0 3085 0 [pid=14299] vsize: 12920 Current children cumulated CPU time (s) 509.78 Current children cumulated vsize (Kb) 15044 [startup+520.065 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14317 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3123 0 0 0 51944 34 0 0 25 0 1 0 1842179479 13230080 3110 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3230 3110 145 145 0 3085 0 [pid=14299] vsize: 12920 Current children cumulated CPU time (s) 519.78 Current children cumulated vsize (Kb) 15044 [startup+530.066 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14317 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3130 0 0 0 52944 34 0 0 25 0 1 0 1842179479 13262848 3117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3238 3117 145 145 0 3093 0 [pid=14299] vsize: 12952 Current children cumulated CPU time (s) 529.78 Current children cumulated vsize (Kb) 15076 [startup+540.067 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14317 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3130 0 0 0 53945 34 0 0 25 0 1 0 1842179479 13262848 3117 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3238 3117 145 145 0 3093 0 [pid=14299] vsize: 12952 Current children cumulated CPU time (s) 539.79 Current children cumulated vsize (Kb) 15076 [startup+550.068 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14317 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3133 0 0 0 54945 34 0 0 25 0 1 0 1842179479 13275136 3120 4294967295 134512640 135094434 3221224448 3221223120 134556236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3241 3120 145 145 0 3096 0 [pid=14299] vsize: 12964 Current children cumulated CPU time (s) 549.79 Current children cumulated vsize (Kb) 15088 [startup+560.069 s] Raw data (loadavg): 0.99 0.96 0.94 2/58 14317 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3159 0 0 0 55945 34 0 0 25 0 1 0 1842179479 13381632 3146 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3267 3146 145 145 0 3122 0 [pid=14299] vsize: 13068 Current children cumulated CPU time (s) 559.79 Current children cumulated vsize (Kb) 15192 [startup+570.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14319 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3159 0 0 0 56945 34 0 0 25 0 1 0 1842179479 13381632 3146 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3267 3146 145 145 0 3122 0 [pid=14299] vsize: 13068 Current children cumulated CPU time (s) 569.79 Current children cumulated vsize (Kb) 15192 [startup+580.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14319 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3223 0 0 0 57944 34 0 0 25 0 1 0 1842179479 13647872 3210 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3332 3210 145 145 0 3187 0 [pid=14299] vsize: 13328 Current children cumulated CPU time (s) 579.78 Current children cumulated vsize (Kb) 15452 [startup+590.071 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14319 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3271 0 0 0 58944 34 0 0 25 0 1 0 1842179479 13844480 3258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3380 3258 145 145 0 3235 0 [pid=14299] vsize: 13520 Current children cumulated CPU time (s) 589.78 Current children cumulated vsize (Kb) 15644 [startup+600.072 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14319 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3279 0 0 0 59944 34 0 0 25 0 1 0 1842179479 13893632 3266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3392 3266 145 145 0 3247 0 [pid=14299] vsize: 13568 Current children cumulated CPU time (s) 599.78 Current children cumulated vsize (Kb) 15692 [startup+610.073 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14319 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3279 0 0 0 60944 34 0 0 25 0 1 0 1842179479 13893632 3266 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 3392 3266 145 145 0 3247 0 [pid=14299] vsize: 13568 Current children cumulated CPU time (s) 609.78 Current children cumulated vsize (Kb) 15692 [startup+620.074 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14319 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3391 0 0 0 61941 35 0 0 25 0 1 0 1842179479 14331904 3378 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 3499 3378 145 145 0 3354 0 [pid=14299] vsize: 13996 Current children cumulated CPU time (s) 619.76 Current children cumulated vsize (Kb) 16120 [startup+630.075 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14321 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3394 0 0 0 62941 36 0 0 25 0 1 0 1842179479 14348288 3381 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3503 3381 145 145 0 3358 0 [pid=14299] vsize: 14012 Current children cumulated CPU time (s) 629.77 Current children cumulated vsize (Kb) 16136 [startup+640.076 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14321 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3495 0 0 0 63939 37 0 0 25 0 1 0 1842179479 14761984 3482 4294967295 134512640 135094434 3221224448 3221223120 134555828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3604 3482 145 145 0 3459 0 [pid=14299] vsize: 14416 Current children cumulated CPU time (s) 639.76 Current children cumulated vsize (Kb) 16540 [startup+650.077 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14321 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3502 0 0 0 64939 37 0 0 25 0 1 0 1842179479 14794752 3489 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3612 3489 145 145 0 3467 0 [pid=14299] vsize: 14448 Current children cumulated CPU time (s) 649.76 Current children cumulated vsize (Kb) 16572 [startup+660.079 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14321 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3571 0 0 0 65937 38 0 0 25 0 1 0 1842179479 15081472 3558 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3682 3558 145 145 0 3537 0 [pid=14299] vsize: 14728 Current children cumulated CPU time (s) 659.75 Current children cumulated vsize (Kb) 16852 [startup+670.08 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14321 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 66937 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0 [pid=14299] vsize: 14792 Current children cumulated CPU time (s) 669.75 Current children cumulated vsize (Kb) 16916 [startup+680.08 s] Raw data (loadavg): 0.99 0.97 0.94 2/58 14321 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 67937 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0 [pid=14299] vsize: 14792 Current children cumulated CPU time (s) 679.75 Current children cumulated vsize (Kb) 16916 [startup+690.081 s] Raw data (loadavg): 1.07 0.99 0.95 2/58 14323 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 68937 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0 [pid=14299] vsize: 14792 Current children cumulated CPU time (s) 689.75 Current children cumulated vsize (Kb) 16916 [startup+700.082 s] Raw data (loadavg): 1.06 0.99 0.95 2/58 14323 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 69938 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0 [pid=14299] vsize: 14792 Current children cumulated CPU time (s) 699.76 Current children cumulated vsize (Kb) 16916 [startup+710.084 s] Raw data (loadavg): 1.05 0.99 0.95 2/58 14323 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 70938 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0 [pid=14299] vsize: 14800 Current children cumulated CPU time (s) 709.76 Current children cumulated vsize (Kb) 16924 [startup+720.085 s] Raw data (loadavg): 1.04 0.99 0.95 2/58 14323 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 71938 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0 [pid=14299] vsize: 14800 Current children cumulated CPU time (s) 719.76 Current children cumulated vsize (Kb) 16924 [startup+730.086 s] Raw data (loadavg): 1.04 0.99 0.95 2/58 14323 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 72938 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0 [pid=14299] vsize: 14800 Current children cumulated CPU time (s) 729.76 Current children cumulated vsize (Kb) 16924 [startup+740.087 s] Raw data (loadavg): 1.03 0.99 0.95 2/58 14323 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 73939 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0 [pid=14299] vsize: 14800 Current children cumulated CPU time (s) 739.77 Current children cumulated vsize (Kb) 16924 [startup+750.088 s] Raw data (loadavg): 1.11 1.00 0.95 2/58 14325 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3594 0 0 0 74939 38 0 0 25 0 1 0 1842179479 15204352 3581 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3712 3581 145 145 0 3567 0 [pid=14299] vsize: 14848 Current children cumulated CPU time (s) 749.77 Current children cumulated vsize (Kb) 16972 [startup+760.09 s] Raw data (loadavg): 1.09 1.00 0.95 2/58 14325 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3600 0 0 0 75939 38 0 0 25 0 1 0 1842179479 15224832 3587 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3717 3587 145 145 0 3572 0 [pid=14299] vsize: 14868 Current children cumulated CPU time (s) 759.77 Current children cumulated vsize (Kb) 16992 [startup+770.091 s] Raw data (loadavg): 1.07 1.00 0.95 2/58 14325 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3628 0 0 0 76939 38 0 0 25 0 1 0 1842179479 15339520 3615 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3745 3615 145 145 0 3600 0 [pid=14299] vsize: 14980 Current children cumulated CPU time (s) 769.77 Current children cumulated vsize (Kb) 17104 [startup+780.092 s] Raw data (loadavg): 1.06 1.00 0.95 2/58 14325 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 77939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0 [pid=14299] vsize: 15080 Current children cumulated CPU time (s) 779.78 Current children cumulated vsize (Kb) 17204 [startup+790.093 s] Raw data (loadavg): 1.05 1.00 0.95 2/58 14325 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 78939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223008 134550333 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0 [pid=14299] vsize: 15080 Current children cumulated CPU time (s) 789.78 Current children cumulated vsize (Kb) 17204 [startup+800.094 s] Raw data (loadavg): 1.04 1.00 0.95 2/58 14325 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 79939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0 [pid=14299] vsize: 15080 Current children cumulated CPU time (s) 799.78 Current children cumulated vsize (Kb) 17204 [startup+810.095 s] Raw data (loadavg): 1.04 1.00 0.95 2/58 14327 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 80939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0 [pid=14299] vsize: 15080 Current children cumulated CPU time (s) 809.78 Current children cumulated vsize (Kb) 17204 [startup+820.095 s] Raw data (loadavg): 1.03 1.00 0.95 2/58 14327 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3656 0 0 0 81940 39 0 0 25 0 1 0 1842179479 15454208 3643 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3773 3643 145 145 0 3628 0 [pid=14299] vsize: 15092 Current children cumulated CPU time (s) 819.79 Current children cumulated vsize (Kb) 17216 [startup+830.096 s] Raw data (loadavg): 1.03 1.00 0.95 2/58 14327 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3671 0 0 0 82940 39 0 0 25 0 1 0 1842179479 15515648 3658 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3788 3658 145 145 0 3643 0 [pid=14299] vsize: 15152 Current children cumulated CPU time (s) 829.79 Current children cumulated vsize (Kb) 17276 [startup+840.097 s] Raw data (loadavg): 1.02 1.00 0.95 2/58 14327 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3675 0 0 0 83940 39 0 0 25 0 1 0 1842179479 15532032 3662 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3792 3662 145 145 0 3647 0 [pid=14299] vsize: 15168 Current children cumulated CPU time (s) 839.79 Current children cumulated vsize (Kb) 17292 [startup+850.098 s] Raw data (loadavg): 1.02 1.00 0.95 2/58 14327 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3680 0 0 0 84940 39 0 0 25 0 1 0 1842179479 15552512 3667 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3797 3667 145 145 0 3652 0 [pid=14299] vsize: 15188 Current children cumulated CPU time (s) 849.79 Current children cumulated vsize (Kb) 17312 [startup+860.1 s] Raw data (loadavg): 1.01 1.00 0.95 2/58 14327 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3680 0 0 0 85940 39 0 0 25 0 1 0 1842179479 15552512 3667 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3797 3667 145 145 0 3652 0 [pid=14299] vsize: 15188 Current children cumulated CPU time (s) 859.79 Current children cumulated vsize (Kb) 17312 [startup+870.101 s] Raw data (loadavg): 1.01 1.00 0.95 2/58 14329 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 86941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0 [pid=14299] vsize: 15204 Current children cumulated CPU time (s) 869.8 Current children cumulated vsize (Kb) 17328 [startup+880.102 s] Raw data (loadavg): 1.01 1.00 0.95 2/58 14329 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 87941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0 [pid=14299] vsize: 15204 Current children cumulated CPU time (s) 879.8 Current children cumulated vsize (Kb) 17328 [startup+890.103 s] Raw data (loadavg): 1.01 1.00 0.95 2/58 14329 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 88941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0 [pid=14299] vsize: 15204 Current children cumulated CPU time (s) 889.8 Current children cumulated vsize (Kb) 17328 [startup+900.104 s] Raw data (loadavg): 1.01 1.00 0.95 2/58 14329 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 89941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0 [pid=14299] vsize: 15204 Current children cumulated CPU time (s) 899.8 Current children cumulated vsize (Kb) 17328 [startup+910.106 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14329 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3732 0 0 0 90941 39 0 0 25 0 1 0 1842179479 15765504 3719 4294967295 134512640 135094434 3221224448 3221223008 134550329 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3849 3719 145 145 0 3704 0 [pid=14299] vsize: 15396 Current children cumulated CPU time (s) 909.8 Current children cumulated vsize (Kb) 17520 [startup+920.107 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14329 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3732 0 0 0 91941 39 0 0 25 0 1 0 1842179479 15765504 3719 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3849 3719 145 145 0 3704 0 [pid=14299] vsize: 15396 Current children cumulated CPU time (s) 919.8 Current children cumulated vsize (Kb) 17520 [startup+930.108 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14331 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 92940 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0 [pid=14299] vsize: 15584 Current children cumulated CPU time (s) 929.8 Current children cumulated vsize (Kb) 17708 [startup+940.109 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14331 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 93941 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0 [pid=14299] vsize: 15584 Current children cumulated CPU time (s) 939.81 Current children cumulated vsize (Kb) 17708 [startup+950.11 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14331 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 94941 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0 [pid=14299] vsize: 15584 Current children cumulated CPU time (s) 949.81 Current children cumulated vsize (Kb) 17708 [startup+960.111 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14331 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 95941 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0 [pid=14299] vsize: 15584 Current children cumulated CPU time (s) 959.81 Current children cumulated vsize (Kb) 17708 [startup+970.112 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14331 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3864 0 0 0 96938 41 0 0 25 0 1 0 1842179479 16310272 3851 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 3982 3851 145 145 0 3837 0 [pid=14299] vsize: 15928 Current children cumulated CPU time (s) 969.79 Current children cumulated vsize (Kb) 18052 [startup+980.113 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14331 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3870 0 0 0 97938 42 0 0 25 0 1 0 1842179479 16343040 3857 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 3990 3857 145 145 0 3845 0 [pid=14299] vsize: 15960 Current children cumulated CPU time (s) 979.8 Current children cumulated vsize (Kb) 18084 [startup+990.114 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14333 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3876 0 0 0 98937 43 0 0 25 0 1 0 1842179479 16367616 3863 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 3996 3863 145 145 0 3851 0 [pid=14299] vsize: 15984 Current children cumulated CPU time (s) 989.8 Current children cumulated vsize (Kb) 18108 [startup+1000.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14333 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3884 0 0 0 99936 44 0 0 25 0 1 0 1842179479 16416768 3871 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4008 3871 145 145 0 3863 0 [pid=14299] vsize: 16032 Current children cumulated CPU time (s) 999.8 Current children cumulated vsize (Kb) 18156 [startup+1010.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14333 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3887 0 0 0 100935 44 0 0 25 0 1 0 1842179479 16429056 3874 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4011 3874 145 145 0 3866 0 [pid=14299] vsize: 16044 Current children cumulated CPU time (s) 1009.79 Current children cumulated vsize (Kb) 18168 [startup+1020.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14333 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3890 0 0 0 101935 45 0 0 25 0 1 0 1842179479 16445440 3877 4294967295 134512640 135094434 3221224448 3221223120 134555169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4015 3877 145 145 0 3870 0 [pid=14299] vsize: 16060 Current children cumulated CPU time (s) 1019.8 Current children cumulated vsize (Kb) 18184 [startup+1030.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14333 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 102935 45 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0 [pid=14299] vsize: 16068 Current children cumulated CPU time (s) 1029.8 Current children cumulated vsize (Kb) 18192 [startup+1040.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14333 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 103935 45 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0 [pid=14299] vsize: 16068 Current children cumulated CPU time (s) 1039.8 Current children cumulated vsize (Kb) 18192 [startup+1050.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14335 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 104934 46 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0 [pid=14299] vsize: 16068 Current children cumulated CPU time (s) 1049.8 Current children cumulated vsize (Kb) 18192 [startup+1060.12 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14335 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 105934 46 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0 [pid=14299] vsize: 16068 Current children cumulated CPU time (s) 1059.8 Current children cumulated vsize (Kb) 18192 [startup+1070.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14335 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3909 0 0 0 106934 47 0 0 25 0 1 0 1842179479 16519168 3896 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4033 3896 145 145 0 3888 0 [pid=14299] vsize: 16132 Current children cumulated CPU time (s) 1069.81 Current children cumulated vsize (Kb) 18256 [startup+1080.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14335 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3913 0 0 0 107933 47 0 0 25 0 1 0 1842179479 16535552 3900 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4037 3900 145 145 0 3892 0 [pid=14299] vsize: 16148 Current children cumulated CPU time (s) 1079.8 Current children cumulated vsize (Kb) 18272 [startup+1090.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14335 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3949 0 0 0 108932 48 0 0 25 0 1 0 1842179479 16683008 3936 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4073 3936 145 145 0 3928 0 [pid=14299] vsize: 16292 Current children cumulated CPU time (s) 1089.8 Current children cumulated vsize (Kb) 18416 [startup+1100.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14335 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3953 0 0 0 109932 48 0 0 25 0 1 0 1842179479 16699392 3940 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14299/statm): 4077 3940 145 145 0 3932 0 [pid=14299] vsize: 16308 Current children cumulated CPU time (s) 1099.8 Current children cumulated vsize (Kb) 18432 [startup+1110.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14337 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4009 0 0 0 110930 49 0 0 25 0 1 0 1842179479 16928768 3996 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4133 3996 145 145 0 3988 0 [pid=14299] vsize: 16532 Current children cumulated CPU time (s) 1109.79 Current children cumulated vsize (Kb) 18656 [startup+1120.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14337 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4013 0 0 0 111930 49 0 0 25 0 1 0 1842179479 16945152 4000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4137 4000 145 145 0 3992 0 [pid=14299] vsize: 16548 Current children cumulated CPU time (s) 1119.79 Current children cumulated vsize (Kb) 18672 [startup+1130.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14337 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4030 0 0 0 112930 49 0 0 25 0 1 0 1842179479 17027072 4017 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4157 4017 145 145 0 4012 0 [pid=14299] vsize: 16628 Current children cumulated CPU time (s) 1129.79 Current children cumulated vsize (Kb) 18752 [startup+1140.13 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14337 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4030 0 0 0 113931 49 0 0 25 0 1 0 1842179479 17027072 4017 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4157 4017 145 145 0 4012 0 [pid=14299] vsize: 16628 Current children cumulated CPU time (s) 1139.8 Current children cumulated vsize (Kb) 18752 [startup+1150.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14337 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 114931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0 [pid=14299] vsize: 16660 Current children cumulated CPU time (s) 1149.81 Current children cumulated vsize (Kb) 18784 [startup+1160.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14337 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 115931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0 [pid=14299] vsize: 16660 Current children cumulated CPU time (s) 1159.81 Current children cumulated vsize (Kb) 18784 [startup+1170.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14339 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 116931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0 [pid=14299] vsize: 16660 Current children cumulated CPU time (s) 1169.81 Current children cumulated vsize (Kb) 18784 [startup+1180.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14339 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 117931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0 [pid=14299] vsize: 16660 Current children cumulated CPU time (s) 1179.81 Current children cumulated vsize (Kb) 18784 [startup+1190.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14339 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4058 0 0 0 118931 50 0 0 25 0 1 0 1842179479 17154048 4045 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4188 4045 145 145 0 4043 0 [pid=14299] vsize: 16752 Current children cumulated CPU time (s) 1189.81 Current children cumulated vsize (Kb) 18876 [startup+1200.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14339 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4061 0 0 0 119931 50 0 0 25 0 1 0 1842179479 17170432 4048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4192 4048 145 145 0 4047 0 [pid=14299] vsize: 16768 Current children cumulated CPU time (s) 1199.81 Current children cumulated vsize (Kb) 18892 [startup+1210.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14339 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4062 0 0 0 120932 50 0 0 25 0 1 0 1842179479 17170432 4049 4294967295 134512640 135094434 3221224448 3221223120 134556502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4192 4049 145 145 0 4047 0 [pid=14299] vsize: 16768 Current children cumulated CPU time (s) 1209.82 Current children cumulated vsize (Kb) 18892 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.14 s] Raw data (loadavg): 1.00 1.00 0.95 2/58 14339 Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14295/statm): 531 226 485 147 0 384 0 [pid=14295] vsize: 2124 Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4062 0 0 0 120932 50 0 0 25 0 1 0 1842179479 17170432 4049 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14299/statm): 4192 4049 145 145 0 4047 0 [pid=14299] vsize: 16768 Current children cumulated CPU time (s) 1209.82 Current children cumulated vsize (Kb) 18892 Sending SIGTERM to -14295 Sleeping 2 seconds One traced child (pid=14295) ended because it received signal 15 (SIGTERM) One traced child (pid=14299) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.15 CPU time (s): 1209.83 CPU user time (s): 1209.32 CPU system time (s): 0.509922 CPU usage (%): 99.9734 Max. virtual memory (cumulated for all children) (Kb): 18892
ERROR: no interpretation found !