Name | submitted/aloul/FPGA_SAT05/normalized-chnl50_51_pb.cnf.cr.opb |
MD5SUM | 00bdc6bb9bafd4b1100d8bfa4f886626 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 52 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.173973 |
Number of variables | 5100 |
Total number of constraints | 202 |
Number of constraints which are clauses | 102 |
Number of constraints which are cardinality constraints (but not clauses) | 100 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 50 |
Maximum length of a constraint | 51 |
LAUNCH ON wulflinc15 THE 2005-09-18 12:28:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2361 boxname=wulflinc15 idbench=17 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 00bdc6bb9bafd4b1100d8bfa4f886626 /oldhome/oroussel/tmp/wulflinc15/normalized-chnl50_51_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-chnl50_51_pb.cnf.cr.opb IDLAUNCH: 2361 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 938296 kB Buffers: 35344 kB Cached: 32100 kB SwapCached: 692 kB Active: 53464 kB Inactive: 16572 kB HighTotal: 131008 kB HighFree: 95676 kB LowTotal: 903652 kB LowFree: 842620 kB SwapTotal: 2097136 kB SwapFree: 2095920 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5724 kB Slab: 20668 kB Committed_AS: 64152 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:48:25 (client local time) WITH STATUS 0 IN 1207.08 SECONDS stats: 2361 7 1207.08 0
c Parsing PB file... c Converting 202 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................................................... c ---[ 99]---> BDD-cost: 99 c ---[ 98]---> BDD-cost: 99 c ---[ 97]---> BDD-cost: 99 c ---[ 96]---> BDD-cost: 99 c ---[ 95]---> BDD-cost: 99 c ---[ 94]---> BDD-cost: 99 c ---[ 93]---> BDD-cost: 99 c ---[ 92]---> BDD-cost: 99 c ---[ 91]---> BDD-cost: 99 c ---[ 90]---> BDD-cost: 99 c ---[ 89]---> BDD-cost: 99 c ---[ 88]---> BDD-cost: 99 c ---[ 87]---> BDD-cost: 99 c ---[ 86]---> BDD-cost: 99 c ---[ 85]---> BDD-cost: 99 c ---[ 84]---> BDD-cost: 99 c ---[ 83]---> BDD-cost: 99 c ---[ 82]---> BDD-cost: 99 c ---[ 81]---> BDD-cost: 99 c ---[ 80]---> BDD-cost: 99 c ---[ 79]---> BDD-cost: 99 c ---[ 78]---> BDD-cost: 99 c ---[ 77]---> BDD-cost: 99 c ---[ 76]---> BDD-cost: 99 c ---[ 75]---> BDD-cost: 99 c ---[ 74]---> BDD-cost: 99 c ---[ 73]---> BDD-cost: 99 c ---[ 72]---> BDD-cost: 99 c ---[ 71]---> BDD-cost: 99 c ---[ 70]---> BDD-cost: 99 c ---[ 69]---> BDD-cost: 99 c ---[ 68]---> BDD-cost: 99 c ---[ 67]---> BDD-cost: 99 c ---[ 66]---> BDD-cost: 99 c ---[ 65]---> BDD-cost: 99 c ---[ 64]---> BDD-cost: 99 c ---[ 63]---> BDD-cost: 99 c ---[ 62]---> BDD-cost: 99 c ---[ 61]---> BDD-cost: 99 c ---[ 60]---> BDD-cost: 99 c ---[ 59]---> BDD-cost: 99 c ---[ 58]---> BDD-cost: 99 c ---[ 57]---> BDD-cost: 99 c ---[ 56]---> BDD-cost: 99 c ---[ 55]---> BDD-cost: 99 c ---[ 54]---> BDD-cost: 99 c ---[ 53]---> BDD-cost: 99 c ---[ 52]---> BDD-cost: 99 c ---[ 51]---> BDD-cost: 99 c ---[ 50]---> BDD-cost: 99 c ---[ 49]---> BDD-cost: 99 c ---[ 48]---> BDD-cost: 99 c ---[ 47]---> BDD-cost: 99 c ---[ 46]---> BDD-cost: 99 c ---[ 45]---> BDD-cost: 99 c ---[ 44]---> BDD-cost: 99 c ---[ 43]---> BDD-cost: 99 c ---[ 42]---> BDD-cost: 99 c ---[ 41]---> BDD-cost: 99 c ---[ 40]---> BDD-cost: 99 c ---[ 39]---> BDD-cost: 99 c ---[ 38]---> BDD-cost: 99 c ---[ 37]---> BDD-cost: 99 c ---[ 36]---> BDD-cost: 99 c ---[ 35]---> BDD-cost: 99 c ---[ 34]---> BDD-cost: 99 c ---[ 33]---> BDD-cost: 99 c ---[ 32]---> BDD-cost: 99 c ---[ 31]---> BDD-cost: 99 c ---[ 30]---> BDD-cost: 99 c ---[ 29]---> BDD-cost: 99 c ---[ 28]---> BDD-cost: 99 c ---[ 27]---> BDD-cost: 99 c ---[ 26]---> BDD-cost: 99 c ---[ 25]---> BDD-cost: 99 c ---[ 24]---> BDD-cost: 99 c ---[ 23]---> BDD-cost: 99 c ---[ 22]---> BDD-cost: 99 c ---[ 21]---> BDD-cost: 99 c ---[ 20]---> BDD-cost: 99 c ---[ 19]---> BDD-cost: 99 c ---[ 18]---> BDD-cost: 99 c ---[ 17]---> BDD-cost: 99 c ---[ 16]---> BDD-cost: 99 c ---[ 15]---> BDD-cost: 99 c ---[ 14]---> BDD-cost: 99 c ---[ 13]---> BDD-cost: 99 c ---[ 12]---> BDD-cost: 99 c ---[ 11]---> BDD-cost: 99 c ---[ 10]---> BDD-cost: 99 c ---[ 9]---> BDD-cost: 99 c ---[ 8]---> BDD-cost: 99 c ---[ 7]---> BDD-cost: 99 c ---[ 6]---> BDD-cost: 99 c ---[ 5]---> BDD-cost: 99 c ---[ 4]---> BDD-cost: 99 c ---[ 3]---> BDD-cost: 99 c ---[ 2]---> BDD-cost: 99 c ---[ 1]---> BDD-cost: 99 c ---[ 0]---> BDD-cost: 99 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 24702 69100 | 8234 0 0 nan | 0.000 % | c | 103 | 24702 69100 | 9057 103 21251 206.3 | 0.667 % | c | 257 | 24702 69100 | 9963 257 49705 193.4 | 0.667 % | c | 483 | 24702 69100 | 10959 483 104379 216.1 | 0.667 % | c | 820 | 24702 69100 | 12055 820 161617 197.1 | 0.667 % | c | 1328 | 24702 69100 | 13260 1328 304812 229.5 | 0.667 % | c | 2087 | 24702 69100 | 14587 2087 499248 239.2 | 0.667 % | c | 3226 | 24702 69100 | 16045 3226 939931 291.4 | 0.667 % | c | 4934 | 24702 69100 | 17650 4934 1692679 343.1 | 0.667 % | c | 7497 | 24702 69100 | 19415 7497 2867483 382.5 | 0.667 % | c | 11345 | 24702 69100 | 21356 11345 4334050 382.0 | 0.667 % | c | 17113 | 24702 69100 | 23492 17113 7407340 432.8 | 0.667 % | c | 25762 | 24702 69100 | 25841 25762 11735963 455.6 | 0.667 % | c | 38736 | 24702 69100 | 28426 19007 8582103 451.5 | 0.667 % | c | 58197 | 24702 69100 | 31268 16084 9622847 598.3 | 0.667 % | c | 87391 | 24702 69100 | 34395 15805 8643661 546.9 | 0.667 % | c | 131182 | 24702 69100 | 37835 29400 20102392 683.8 | 0.667 % |
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/1973/stat): 1973 (minisat+_script) R 1972 1973 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783017883 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/1973/statm): 174 3 169 147 0 27 0 [pid=1973] 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=1974 New process pid=1975 New process pid=1976 execve syscall for /bin/sed executable One traced child (pid=1975) 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=1976) exited with status: 0 One traced child (pid=1974) exited with status: 0 New process pid=1977 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-chnl50_51_pb.cnf.cr.opb [startup+10.0048 s] Raw data (loadavg): 0.93 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 3112 0 2 0 948 13 0 0 25 0 1 0 1783017888 13193216 3097 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 3221 3097 145 145 0 3076 0 [pid=1977] vsize: 12884 Current children cumulated CPU time (s) 9.62 Current children cumulated vsize (Kb) 15008 [startup+20.0066 s] Raw data (loadavg): 0.94 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 4854 0 2 0 1922 25 0 0 25 0 1 0 1783017888 20348928 4839 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 4968 4839 145 145 0 4823 0 [pid=1977] vsize: 19872 Current children cumulated CPU time (s) 19.48 Current children cumulated vsize (Kb) 21996 [startup+30.0095 s] Raw data (loadavg): 0.95 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 6469 0 2 0 2901 34 0 0 25 0 1 0 1783017888 26943488 6454 4294967295 134512640 135094434 3221224432 3221223024 134557244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 6578 6454 145 145 0 6433 0 [pid=1977] vsize: 26312 Current children cumulated CPU time (s) 29.36 Current children cumulated vsize (Kb) 28436 [startup+40.0113 s] Raw data (loadavg): 0.96 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 8159 0 2 0 3878 43 0 0 25 0 1 0 1783017888 33857536 8144 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 8266 8144 145 145 0 8121 0 [pid=1977] vsize: 33064 Current children cumulated CPU time (s) 39.22 Current children cumulated vsize (Kb) 35188 [startup+50.0121 s] Raw data (loadavg): 0.96 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 9633 0 2 0 4858 52 0 0 25 0 1 0 1783017888 39948288 9618 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 9753 9618 145 145 0 9608 0 [pid=1977] vsize: 39012 Current children cumulated CPU time (s) 49.11 Current children cumulated vsize (Kb) 41136 [startup+60.0119 s] Raw data (loadavg): 0.97 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 10849 0 2 0 5840 59 0 0 25 0 1 0 1783017888 44924928 10834 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 10968 10834 145 145 0 10823 0 [pid=1977] vsize: 43872 Current children cumulated CPU time (s) 59 Current children cumulated vsize (Kb) 45996 [startup+70.0127 s] Raw data (loadavg): 0.97 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 12077 0 2 0 6823 66 0 0 25 0 1 0 1783017888 49963008 12062 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 12198 12062 145 145 0 12053 0 [pid=1977] vsize: 48792 Current children cumulated CPU time (s) 68.9 Current children cumulated vsize (Kb) 50916 [startup+80.0136 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 13030 0 2 0 7808 73 0 0 25 0 1 0 1783017888 53874688 13015 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 13153 13015 145 145 0 13008 0 [pid=1977] vsize: 52612 Current children cumulated CPU time (s) 78.82 Current children cumulated vsize (Kb) 54736 [startup+90.0144 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 14276 0 2 0 8790 81 0 0 25 0 1 0 1783017888 58970112 14261 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 14397 14261 145 145 0 14252 0 [pid=1977] vsize: 57588 Current children cumulated CPU time (s) 88.72 Current children cumulated vsize (Kb) 59712 [startup+100.015 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 15419 0 2 0 9773 88 0 0 25 0 1 0 1783017888 63651840 15404 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 15540 15404 145 145 0 15395 0 [pid=1977] vsize: 62160 Current children cumulated CPU time (s) 98.62 Current children cumulated vsize (Kb) 64284 [startup+110.016 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16048 0 2 0 10765 90 0 0 25 0 1 0 1783017888 66240512 16033 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16033 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 108.56 Current children cumulated vsize (Kb) 66812 [startup+120.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 11765 90 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 118.56 Current children cumulated vsize (Kb) 66812 [startup+130.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 12765 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 128.57 Current children cumulated vsize (Kb) 66812 [startup+140.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 13764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 138.56 Current children cumulated vsize (Kb) 66812 [startup+150.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 14764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 148.56 Current children cumulated vsize (Kb) 66812 [startup+160.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 15764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 158.56 Current children cumulated vsize (Kb) 66812 [startup+170.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 16764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 168.56 Current children cumulated vsize (Kb) 66812 [startup+180.022 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 17765 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134557185 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 178.57 Current children cumulated vsize (Kb) 66812 [startup+190.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 18765 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 188.57 Current children cumulated vsize (Kb) 66812 [startup+200.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 19765 92 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0 [pid=1977] vsize: 64688 Current children cumulated CPU time (s) 198.58 Current children cumulated vsize (Kb) 66812 [startup+210.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16137 0 2 0 20763 92 0 0 25 0 1 0 1783017888 66592768 16122 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 16258 16122 145 145 0 16113 0 [pid=1977] vsize: 65032 Current children cumulated CPU time (s) 208.56 Current children cumulated vsize (Kb) 67156 [startup+220.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16835 0 2 0 21753 96 0 0 25 0 1 0 1783017888 69472256 16820 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 16961 16820 145 145 0 16816 0 [pid=1977] vsize: 67844 Current children cumulated CPU time (s) 218.5 Current children cumulated vsize (Kb) 69968 [startup+230.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 17349 0 2 0 22744 100 0 0 25 0 1 0 1783017888 71639040 17334 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 17490 17334 145 145 0 17345 0 [pid=1977] vsize: 69960 Current children cumulated CPU time (s) 228.45 Current children cumulated vsize (Kb) 72084 [startup+240.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 17848 0 2 0 23736 104 0 0 25 0 1 0 1783017888 73711616 17833 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 17996 17833 145 145 0 17851 0 [pid=1977] vsize: 71984 Current children cumulated CPU time (s) 238.41 Current children cumulated vsize (Kb) 74108 [startup+250.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 18418 0 2 0 24727 108 0 0 25 0 1 0 1783017888 76070912 18403 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 18572 18403 145 145 0 18427 0 [pid=1977] vsize: 74288 Current children cumulated CPU time (s) 248.36 Current children cumulated vsize (Kb) 76412 [startup+260.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 19154 0 2 0 25715 113 0 0 25 0 1 0 1783017888 79085568 19139 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 19308 19139 145 145 0 19163 0 [pid=1977] vsize: 77232 Current children cumulated CPU time (s) 258.29 Current children cumulated vsize (Kb) 79356 [startup+270.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 19672 0 2 0 26707 116 0 0 25 0 1 0 1783017888 81387520 19657 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 19870 19657 145 145 0 19725 0 [pid=1977] vsize: 79480 Current children cumulated CPU time (s) 268.24 Current children cumulated vsize (Kb) 81604 [startup+280.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20186 0 2 0 27699 119 0 0 25 0 1 0 1783017888 83480576 20171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20381 20171 145 145 0 20236 0 [pid=1977] vsize: 81524 Current children cumulated CPU time (s) 278.19 Current children cumulated vsize (Kb) 83648 [startup+290.033 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20657 0 2 0 28691 123 0 0 25 0 1 0 1783017888 85405696 20642 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20851 20642 145 145 0 20706 0 [pid=1977] vsize: 83404 Current children cumulated CPU time (s) 288.15 Current children cumulated vsize (Kb) 85528 [startup+300.034 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 29689 124 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 298.14 Current children cumulated vsize (Kb) 85804 [startup+310.033 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 30689 124 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 308.14 Current children cumulated vsize (Kb) 85804 [startup+320.035 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 31689 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 318.15 Current children cumulated vsize (Kb) 85804 [startup+330.036 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 32688 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 328.14 Current children cumulated vsize (Kb) 85804 [startup+340.037 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 33688 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 338.14 Current children cumulated vsize (Kb) 85804 [startup+350.039 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 34688 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 348.14 Current children cumulated vsize (Kb) 85804 [startup+360.04 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 35687 126 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 358.14 Current children cumulated vsize (Kb) 85804 [startup+370.04 s] Raw data (loadavg): 1.07 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 36687 126 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134551922 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0 [pid=1977] vsize: 83680 Current children cumulated CPU time (s) 368.14 Current children cumulated vsize (Kb) 85804 [startup+380.041 s] Raw data (loadavg): 1.14 1.02 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 21000 0 2 0 37683 127 0 0 25 0 1 0 1783017888 86802432 20985 4294967295 134512640 135094434 3221224432 3221223024 134556980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 21192 20985 145 145 0 21047 0 [pid=1977] vsize: 84768 Current children cumulated CPU time (s) 378.11 Current children cumulated vsize (Kb) 86892 [startup+390.043 s] Raw data (loadavg): 1.11 1.02 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 22079 0 2 0 38667 135 0 0 25 0 1 0 1783017888 91262976 22064 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 22281 22064 145 145 0 22136 0 [pid=1977] vsize: 89124 Current children cumulated CPU time (s) 388.03 Current children cumulated vsize (Kb) 91248 [startup+400.044 s] Raw data (loadavg): 1.10 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 23255 0 2 0 39651 140 0 0 25 0 1 0 1783017888 96088064 23240 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 23459 23240 145 145 0 23314 0 [pid=1977] vsize: 93836 Current children cumulated CPU time (s) 397.92 Current children cumulated vsize (Kb) 95960 [startup+410.045 s] Raw data (loadavg): 1.08 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 24271 0 2 0 40635 146 0 0 25 0 1 0 1783017888 100274176 24256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 24481 24256 145 145 0 24336 0 [pid=1977] vsize: 97924 Current children cumulated CPU time (s) 407.82 Current children cumulated vsize (Kb) 100048 [startup+420.046 s] Raw data (loadavg): 1.07 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 25301 0 2 0 41620 153 0 0 25 0 1 0 1783017888 104517632 25286 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 25517 25286 145 145 0 25372 0 [pid=1977] vsize: 102068 Current children cumulated CPU time (s) 417.74 Current children cumulated vsize (Kb) 104192 [startup+430.047 s] Raw data (loadavg): 1.06 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 26155 0 2 0 42607 158 0 0 25 0 1 0 1783017888 108044288 26140 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 26378 26140 145 145 0 26233 0 [pid=1977] vsize: 105512 Current children cumulated CPU time (s) 427.66 Current children cumulated vsize (Kb) 107636 [startup+440.049 s] Raw data (loadavg): 1.05 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 27219 0 2 0 43590 167 0 0 25 0 1 0 1783017888 112406528 27204 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 27443 27204 145 145 0 27298 0 [pid=1977] vsize: 109772 Current children cumulated CPU time (s) 437.58 Current children cumulated vsize (Kb) 111896 [startup+450.05 s] Raw data (loadavg): 1.04 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28143 0 2 0 44576 172 0 0 25 0 1 0 1783017888 116191232 28128 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28367 28128 145 145 0 28222 0 [pid=1977] vsize: 113468 Current children cumulated CPU time (s) 447.49 Current children cumulated vsize (Kb) 115592 [startup+460.051 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28771 0 2 0 45565 176 0 0 25 0 1 0 1783017888 118767616 28756 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28756 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 457.42 Current children cumulated vsize (Kb) 118108 [startup+470.052 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28772 0 2 0 46565 176 0 0 25 0 1 0 1783017888 118767616 28757 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28757 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 467.42 Current children cumulated vsize (Kb) 118108 [startup+480.052 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 47565 176 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 477.42 Current children cumulated vsize (Kb) 118108 [startup+490.054 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 48565 177 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 487.43 Current children cumulated vsize (Kb) 118108 [startup+500.055 s] Raw data (loadavg): 1.02 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 49564 177 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 497.42 Current children cumulated vsize (Kb) 118108 [startup+510.056 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 50564 177 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 507.42 Current children cumulated vsize (Kb) 118108 [startup+520.057 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 51564 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 517.43 Current children cumulated vsize (Kb) 118108 [startup+530.058 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 52563 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 527.42 Current children cumulated vsize (Kb) 118108 [startup+540.059 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 53563 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 537.42 Current children cumulated vsize (Kb) 118108 [startup+550.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 54563 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 547.42 Current children cumulated vsize (Kb) 118108 [startup+560.061 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 55562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 557.42 Current children cumulated vsize (Kb) 118108 [startup+570.062 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 56562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 567.42 Current children cumulated vsize (Kb) 118108 [startup+580.063 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 57562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 577.42 Current children cumulated vsize (Kb) 118108 [startup+590.064 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 58562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 587.42 Current children cumulated vsize (Kb) 118108 [startup+600.066 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 59562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 597.42 Current children cumulated vsize (Kb) 118108 [startup+610.066 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 60562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 607.42 Current children cumulated vsize (Kb) 118108 [startup+620.067 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 61561 180 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0 [pid=1977] vsize: 115984 Current children cumulated CPU time (s) 617.42 Current children cumulated vsize (Kb) 118108 [startup+630.068 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29029 0 2 0 62556 182 0 0 25 0 1 0 1783017888 119816192 29014 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 29252 29014 145 145 0 29107 0 [pid=1977] vsize: 117008 Current children cumulated CPU time (s) 627.39 Current children cumulated vsize (Kb) 119132 [startup+640.068 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29434 0 2 0 63550 185 0 0 25 0 1 0 1783017888 121475072 29419 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29419 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 637.36 Current children cumulated vsize (Kb) 120752 [startup+650.069 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29434 0 2 0 64550 186 0 0 25 0 1 0 1783017888 121475072 29419 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29419 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 647.37 Current children cumulated vsize (Kb) 120752 [startup+660.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 65550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 657.37 Current children cumulated vsize (Kb) 120752 [startup+670.071 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 66550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 667.37 Current children cumulated vsize (Kb) 120752 [startup+680.072 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 67550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 677.37 Current children cumulated vsize (Kb) 120752 [startup+690.073 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 68550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 687.37 Current children cumulated vsize (Kb) 120752 [startup+700.073 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 69550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 697.38 Current children cumulated vsize (Kb) 120752 [startup+710.074 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 70550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 707.38 Current children cumulated vsize (Kb) 120752 [startup+720.075 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 71550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 717.38 Current children cumulated vsize (Kb) 120752 [startup+730.076 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 72549 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 727.37 Current children cumulated vsize (Kb) 120752 [startup+740.078 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 73550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 737.38 Current children cumulated vsize (Kb) 120752 [startup+750.079 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 74550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 747.38 Current children cumulated vsize (Kb) 120752 [startup+760.078 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 75550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0 [pid=1977] vsize: 118628 Current children cumulated CPU time (s) 757.38 Current children cumulated vsize (Kb) 120752 [startup+770.079 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 30207 0 2 0 76540 192 0 0 25 0 1 0 1783017888 124657664 30192 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 30434 30192 145 145 0 30289 0 [pid=1977] vsize: 121736 Current children cumulated CPU time (s) 767.33 Current children cumulated vsize (Kb) 123860 [startup+780.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 31112 0 2 0 77526 198 0 0 25 0 1 0 1783017888 128368640 31097 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 31340 31097 145 145 0 31195 0 [pid=1977] vsize: 125360 Current children cumulated CPU time (s) 777.25 Current children cumulated vsize (Kb) 127484 [startup+790.081 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) T 1973 1973 31778 0 -1 0 32021 0 2 0 78513 204 0 0 25 0 1 0 1783017888 132087808 32006 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/1977/statm): 32248 32006 145 145 0 32103 0 [pid=1977] vsize: 128992 Current children cumulated CPU time (s) 787.18 Current children cumulated vsize (Kb) 131116 [startup+800.082 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 32803 0 2 0 79502 209 0 0 25 0 1 0 1783017888 135360512 32788 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 33047 32788 145 145 0 32902 0 [pid=1977] vsize: 132188 Current children cumulated CPU time (s) 797.12 Current children cumulated vsize (Kb) 134312 [startup+810.082 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 33575 0 2 0 80492 213 0 0 22 0 1 0 1783017888 138616832 33560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 33842 33560 145 145 0 33697 0 [pid=1977] vsize: 135368 Current children cumulated CPU time (s) 807.06 Current children cumulated vsize (Kb) 137492 [startup+820.083 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34346 0 2 0 81480 218 0 0 25 0 1 0 1783017888 141791232 34331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 34617 34331 145 145 0 34472 0 [pid=1977] vsize: 138468 Current children cumulated CPU time (s) 816.99 Current children cumulated vsize (Kb) 140592 [startup+830.084 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34924 0 2 0 82472 221 0 0 25 0 1 0 1783017888 144224256 34909 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34909 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 826.94 Current children cumulated vsize (Kb) 142968 [startup+840.086 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34926 0 2 0 83472 222 0 0 25 0 1 0 1783017888 144224256 34911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34911 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 836.95 Current children cumulated vsize (Kb) 142968 [startup+850.087 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34926 0 2 0 84471 222 0 0 25 0 1 0 1783017888 144224256 34911 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34911 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 846.94 Current children cumulated vsize (Kb) 142968 [startup+860.088 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34927 0 2 0 85471 222 0 0 25 0 1 0 1783017888 144224256 34912 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34912 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 856.94 Current children cumulated vsize (Kb) 142968 [startup+870.089 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34927 0 2 0 86470 223 0 0 25 0 1 0 1783017888 144224256 34912 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34912 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 866.94 Current children cumulated vsize (Kb) 142968 [startup+880.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34932 0 2 0 87470 223 0 0 25 0 1 0 1783017888 144224256 34917 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34917 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 876.94 Current children cumulated vsize (Kb) 142968 [startup+890.092 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34934 0 2 0 88470 223 0 0 25 0 1 0 1783017888 144224256 34919 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34919 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 886.94 Current children cumulated vsize (Kb) 142968 [startup+900.094 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34935 0 2 0 89469 224 0 0 25 0 1 0 1783017888 144224256 34920 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34920 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 896.94 Current children cumulated vsize (Kb) 142968 [startup+910.095 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34935 0 2 0 90469 224 0 0 25 0 1 0 1783017888 144224256 34920 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34920 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 906.94 Current children cumulated vsize (Kb) 142968 [startup+920.097 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34935 0 2 0 91469 224 0 0 25 0 1 0 1783017888 144224256 34920 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34920 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 916.94 Current children cumulated vsize (Kb) 142968 [startup+930.097 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34939 0 2 0 92468 224 0 0 25 0 1 0 1783017888 144224256 34924 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34924 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 926.93 Current children cumulated vsize (Kb) 142968 [startup+940.099 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34939 0 2 0 93468 225 0 0 25 0 1 0 1783017888 144224256 34924 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1977/statm): 35211 34924 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 936.94 Current children cumulated vsize (Kb) 142968 [startup+950.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34942 0 2 0 94468 225 0 0 25 0 1 0 1783017888 144224256 34927 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34927 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 946.94 Current children cumulated vsize (Kb) 142968 [startup+960.101 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34942 0 2 0 95468 225 0 0 25 0 1 0 1783017888 144224256 34927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34927 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 956.94 Current children cumulated vsize (Kb) 142968 [startup+970.103 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34946 0 2 0 96469 225 0 0 25 0 1 0 1783017888 144224256 34931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34931 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 966.95 Current children cumulated vsize (Kb) 142968 [startup+980.103 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34949 0 2 0 97469 225 0 0 25 0 1 0 1783017888 144224256 34934 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34934 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 976.95 Current children cumulated vsize (Kb) 142968 [startup+990.104 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34955 0 2 0 98469 225 0 0 25 0 1 0 1783017888 144224256 34940 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34940 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 986.95 Current children cumulated vsize (Kb) 142968 [startup+1000.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34955 0 2 0 99469 225 0 0 25 0 1 0 1783017888 144224256 34940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34940 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 996.95 Current children cumulated vsize (Kb) 142968 [startup+1010.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34956 0 2 0 100470 225 0 0 25 0 1 0 1783017888 144224256 34941 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34941 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1006.96 Current children cumulated vsize (Kb) 142968 [startup+1020.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 101470 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1016.96 Current children cumulated vsize (Kb) 142968 [startup+1030.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 102470 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1026.96 Current children cumulated vsize (Kb) 142968 [startup+1040.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 103470 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1036.96 Current children cumulated vsize (Kb) 142968 [startup+1050.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 104471 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1046.97 Current children cumulated vsize (Kb) 142968 [startup+1060.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 105471 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1056.97 Current children cumulated vsize (Kb) 142968 [startup+1070.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 106471 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1066.97 Current children cumulated vsize (Kb) 142968 [startup+1080.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 107471 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1076.97 Current children cumulated vsize (Kb) 142968 [startup+1090.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 108472 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1086.98 Current children cumulated vsize (Kb) 142968 [startup+1100.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 109472 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1096.98 Current children cumulated vsize (Kb) 142968 [startup+1110.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34969 0 2 0 110472 225 0 0 25 0 1 0 1783017888 144224256 34954 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34954 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1106.98 Current children cumulated vsize (Kb) 142968 [startup+1120.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34969 0 2 0 111472 225 0 0 25 0 1 0 1783017888 144224256 34954 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34954 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1116.98 Current children cumulated vsize (Kb) 142968 [startup+1130.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34971 0 2 0 112472 225 0 0 25 0 1 0 1783017888 144224256 34956 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34956 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1126.98 Current children cumulated vsize (Kb) 142968 [startup+1140.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34971 0 2 0 113473 225 0 0 25 0 1 0 1783017888 144224256 34956 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34956 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1136.99 Current children cumulated vsize (Kb) 142968 [startup+1150.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 114473 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1146.99 Current children cumulated vsize (Kb) 142968 [startup+1160.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 115473 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1156.99 Current children cumulated vsize (Kb) 142968 [startup+1170.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 116474 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1167 Current children cumulated vsize (Kb) 142968 [startup+1180.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 117474 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1177 Current children cumulated vsize (Kb) 142968 [startup+1190.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 118474 226 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1187.01 Current children cumulated vsize (Kb) 142968 [startup+1200.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 119474 226 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1197.01 Current children cumulated vsize (Kb) 142968 [startup+1210.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34973 0 2 0 120474 226 0 0 25 0 1 0 1783017888 144224256 34958 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34958 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1207.01 Current children cumulated vsize (Kb) 142968 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 1977 Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1973/statm): 531 226 485 147 0 384 0 [pid=1973] vsize: 2124 Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34973 0 2 0 120474 226 0 0 25 0 1 0 1783017888 144224256 34958 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1977/statm): 35211 34958 145 145 0 35066 0 [pid=1977] vsize: 140844 Current children cumulated CPU time (s) 1207.01 Current children cumulated vsize (Kb) 142968 Sending SIGTERM to -1973 Sleeping 2 seconds One traced child (pid=1973) ended because it received signal 15 (SIGTERM) One traced child (pid=1977) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1207.08 CPU user time (s): 1204.75 CPU system time (s): 2.32765 CPU usage (%): 99.7422 Max. virtual memory (cumulated for all children) (Kb): 142968
ERROR: no interpretation found !