Name | submitted/aloul/FPGA_SAT05/normalized-chnl50_55_pb.cnf.cr.opb |
MD5SUM | 88aaed929c30a489c8806c3852596de3 |
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 | 56 |
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.188971 |
Number of variables | 5500 |
Total number of constraints | 210 |
Number of constraints which are clauses | 110 |
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 | 55 |
LAUNCH ON wulflinc26 THE 2005-09-18 12:28:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2362 boxname=wulflinc26 idbench=18 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 88aaed929c30a489c8806c3852596de3 /oldhome/oroussel/tmp/wulflinc26/normalized-chnl50_55_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-chnl50_55_pb.cnf.cr.opb IDLAUNCH: 2362 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 944680 kB Buffers: 34768 kB Cached: 28216 kB SwapCached: 868 kB Active: 53532 kB Inactive: 12080 kB HighTotal: 131008 kB HighFree: 100072 kB LowTotal: 903652 kB LowFree: 844608 kB SwapTotal: 2097892 kB SwapFree: 2096540 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5696 kB Slab: 18756 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 12:48:37 (client local time) WITH STATUS 0 IN 1207.8 SECONDS stats: 2362 7 1207.8 0
c Parsing PB file... c Converting 210 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .............................................................................................................. c ---[ 99]---> BDD-cost: 107 c ---[ 98]---> BDD-cost: 107 c ---[ 97]---> BDD-cost: 107 c ---[ 96]---> BDD-cost: 107 c ---[ 95]---> BDD-cost: 107 c ---[ 94]---> BDD-cost: 107 c ---[ 93]---> BDD-cost: 107 c ---[ 92]---> BDD-cost: 107 c ---[ 91]---> BDD-cost: 107 c ---[ 90]---> BDD-cost: 107 c ---[ 89]---> BDD-cost: 107 c ---[ 88]---> BDD-cost: 107 c ---[ 87]---> BDD-cost: 107 c ---[ 86]---> BDD-cost: 107 c ---[ 85]---> BDD-cost: 107 c ---[ 84]---> BDD-cost: 107 c ---[ 83]---> BDD-cost: 107 c ---[ 82]---> BDD-cost: 107 c ---[ 81]---> BDD-cost: 107 c ---[ 80]---> BDD-cost: 107 c ---[ 79]---> BDD-cost: 107 c ---[ 78]---> BDD-cost: 107 c ---[ 77]---> BDD-cost: 107 c ---[ 76]---> BDD-cost: 107 c ---[ 75]---> BDD-cost: 107 c ---[ 74]---> BDD-cost: 107 c ---[ 73]---> BDD-cost: 107 c ---[ 72]---> BDD-cost: 107 c ---[ 71]---> BDD-cost: 107 c ---[ 70]---> BDD-cost: 107 c ---[ 69]---> BDD-cost: 107 c ---[ 68]---> BDD-cost: 107 c ---[ 67]---> BDD-cost: 107 c ---[ 66]---> BDD-cost: 107 c ---[ 65]---> BDD-cost: 107 c ---[ 64]---> BDD-cost: 107 c ---[ 63]---> BDD-cost: 107 c ---[ 62]---> BDD-cost: 107 c ---[ 61]---> BDD-cost: 107 c ---[ 60]---> BDD-cost: 107 c ---[ 59]---> BDD-cost: 107 c ---[ 58]---> BDD-cost: 107 c ---[ 57]---> BDD-cost: 107 c ---[ 56]---> BDD-cost: 107 c ---[ 55]---> BDD-cost: 107 c ---[ 54]---> BDD-cost: 107 c ---[ 53]---> BDD-cost: 107 c ---[ 52]---> BDD-cost: 107 c ---[ 51]---> BDD-cost: 107 c ---[ 50]---> BDD-cost: 107 c ---[ 49]---> BDD-cost: 107 c ---[ 48]---> BDD-cost: 107 c ---[ 47]---> BDD-cost: 107 c ---[ 46]---> BDD-cost: 107 c ---[ 45]---> BDD-cost: 107 c ---[ 44]---> BDD-cost: 107 c ---[ 43]---> BDD-cost: 107 c ---[ 42]---> BDD-cost: 107 c ---[ 41]---> BDD-cost: 107 c ---[ 40]---> BDD-cost: 107 c ---[ 39]---> BDD-cost: 107 c ---[ 38]---> BDD-cost: 107 c ---[ 37]---> BDD-cost: 107 c ---[ 36]---> BDD-cost: 107 c ---[ 35]---> BDD-cost: 107 c ---[ 34]---> BDD-cost: 107 c ---[ 33]---> BDD-cost: 107 c ---[ 32]---> BDD-cost: 107 c ---[ 31]---> BDD-cost: 107 c ---[ 30]---> BDD-cost: 107 c ---[ 29]---> BDD-cost: 107 c ---[ 28]---> BDD-cost: 107 c ---[ 27]---> BDD-cost: 107 c ---[ 26]---> BDD-cost: 107 c ---[ 25]---> BDD-cost: 107 c ---[ 24]---> BDD-cost: 107 c ---[ 23]---> BDD-cost: 107 c ---[ 22]---> BDD-cost: 107 c ---[ 21]---> BDD-cost: 107 c ---[ 20]---> BDD-cost: 107 c ---[ 19]---> BDD-cost: 107 c ---[ 18]---> BDD-cost: 107 c ---[ 17]---> BDD-cost: 107 c ---[ 16]---> BDD-cost: 107 c ---[ 15]---> BDD-cost: 107 c ---[ 14]---> BDD-cost: 107 c ---[ 13]---> BDD-cost: 107 c ---[ 12]---> BDD-cost: 107 c ---[ 11]---> BDD-cost: 107 c ---[ 10]---> BDD-cost: 107 c ---[ 9]---> BDD-cost: 107 c ---[ 8]---> BDD-cost: 107 c ---[ 7]---> BDD-cost: 107 c ---[ 6]---> BDD-cost: 107 c ---[ 5]---> BDD-cost: 107 c ---[ 4]---> BDD-cost: 107 c ---[ 3]---> BDD-cost: 107 c ---[ 2]---> BDD-cost: 107 c ---[ 1]---> BDD-cost: 107 c ---[ 0]---> BDD-cost: 107 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 26710 74700 | 8903 0 0 nan | 0.000 % | c | 101 | 26710 74700 | 9793 101 19540 193.5 | 0.617 % | c | 254 | 26710 74700 | 10772 254 57136 224.9 | 0.617 % | c | 479 | 26710 74700 | 11849 479 106928 223.2 | 0.617 % | c | 820 | 26710 74700 | 13034 820 228012 278.1 | 0.617 % | c | 1327 | 26710 74700 | 14338 1327 407337 307.0 | 0.617 % | c | 2089 | 26710 74700 | 15772 2089 607183 290.7 | 0.617 % | c | 3232 | 26710 74700 | 17349 3232 926679 286.7 | 0.617 % | c | 4943 | 26710 74700 | 19084 4943 1483658 300.2 | 0.617 % | c | 7507 | 26710 74700 | 20992 7507 2510030 334.4 | 0.617 % | c | 11351 | 26710 74700 | 23092 11351 4018398 354.0 | 0.617 % | c | 17118 | 26710 74700 | 25401 17118 7441464 434.7 | 0.617 % | c | 25771 | 26710 74700 | 27941 25771 13547867 525.7 | 0.617 % | c | 38747 | 26710 74700 | 30735 11992 5242030 437.1 | 0.617 % | c | 58209 | 26710 74700 | 33809 31454 12687777 403.4 | 0.617 % | c | 87404 | 26710 74700 | 37190 27207 15612638 573.8 | 0.617 % | c | 131194 | 26710 74700 | 40909 35274 17941262 508.6 | 0.617 % |
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/19172/stat): 19172 (minisat+_script) R 19171 19172 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841267036 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/19172/statm): 174 3 169 147 0 27 0 [pid=19172] 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=19173 New process pid=19174 New process pid=19175 execve syscall for /bin/sed executable One traced child (pid=19174) 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=19175) exited with status: 0 One traced child (pid=19173) exited with status: 0 New process pid=19176 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-chnl50_55_pb.cnf.cr.opb [startup+10.005 s] Raw data (loadavg): 0.93 0.95 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 3096 0 2 0 950 14 0 0 25 0 1 0 1841267041 12746752 3002 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 3112 3002 145 145 0 2967 0 [pid=19176] vsize: 12448 Current children cumulated CPU time (s) 9.64 Current children cumulated vsize (Kb) 14572 [startup+20.0066 s] Raw data (loadavg): 0.94 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) T 19172 19172 16528 0 -1 0 4624 0 2 0 1927 25 0 0 25 0 1 0 1841267041 19021824 4530 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/19176/statm): 4644 4530 145 145 0 4499 0 [pid=19176] vsize: 18576 Current children cumulated CPU time (s) 19.52 Current children cumulated vsize (Kb) 20700 [startup+30.0073 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 6144 0 2 0 2904 34 0 0 25 0 1 0 1841267041 25235456 6050 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 6161 6050 145 145 0 6016 0 [pid=19176] vsize: 24644 Current children cumulated CPU time (s) 29.38 Current children cumulated vsize (Kb) 26768 [startup+40.008 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 7524 0 2 0 3885 42 0 0 25 0 1 0 1841267041 30875648 7430 4294967295 134512640 135094434 3221224432 3221223104 134555683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 7538 7430 145 145 0 7393 0 [pid=19176] vsize: 30152 Current children cumulated CPU time (s) 39.27 Current children cumulated vsize (Kb) 32276 [startup+50.0107 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 8710 0 2 0 4867 50 0 0 25 0 1 0 1841267041 35794944 8616 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 8739 8616 145 145 0 8594 0 [pid=19176] vsize: 34956 Current children cumulated CPU time (s) 49.17 Current children cumulated vsize (Kb) 37080 [startup+60.0104 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 10062 0 2 0 5846 59 0 0 25 0 1 0 1841267041 41324544 9968 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 10089 9968 145 145 0 9944 0 [pid=19176] vsize: 40356 Current children cumulated CPU time (s) 59.05 Current children cumulated vsize (Kb) 42480 [startup+70.0111 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 11254 0 2 0 6828 68 0 0 25 0 1 0 1841267041 46198784 11160 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 11279 11160 145 145 0 11134 0 [pid=19176] vsize: 45116 Current children cumulated CPU time (s) 68.96 Current children cumulated vsize (Kb) 47240 [startup+80.0118 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 12397 0 2 0 7812 74 0 0 25 0 1 0 1841267041 50876416 12303 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 12421 12303 145 145 0 12276 0 [pid=19176] vsize: 49684 Current children cumulated CPU time (s) 78.86 Current children cumulated vsize (Kb) 51808 [startup+90.0125 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 13437 0 2 0 8798 80 0 0 25 0 1 0 1841267041 55132160 13343 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 13460 13343 145 145 0 13315 0 [pid=19176] vsize: 53840 Current children cumulated CPU time (s) 88.78 Current children cumulated vsize (Kb) 55964 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) T 19172 19172 16528 0 -1 0 14328 0 2 0 9786 86 0 0 25 0 1 0 1841267041 58781696 14234 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/19176/statm): 14351 14234 145 145 0 14206 0 [pid=19176] vsize: 57404 Current children cumulated CPU time (s) 98.72 Current children cumulated vsize (Kb) 59528 [startup+110.014 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 15273 0 2 0 10773 91 0 0 25 0 1 0 1841267041 62656512 15179 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 15297 15179 145 145 0 15152 0 [pid=19176] vsize: 61188 Current children cumulated CPU time (s) 108.64 Current children cumulated vsize (Kb) 63312 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 17290 0 2 0 11751 100 0 0 25 0 1 0 1841267041 70905856 17196 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 17311 17196 145 145 0 17166 0 [pid=19176] vsize: 69244 Current children cumulated CPU time (s) 118.51 Current children cumulated vsize (Kb) 71368 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 18822 0 2 0 12732 108 0 0 25 0 1 0 1841267041 77303808 18728 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 18873 18728 145 145 0 18728 0 [pid=19176] vsize: 75492 Current children cumulated CPU time (s) 128.4 Current children cumulated vsize (Kb) 77616 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 19973 0 2 0 13718 115 0 0 25 0 1 0 1841267041 82014208 19879 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 20023 19879 145 145 0 19878 0 [pid=19176] vsize: 80092 Current children cumulated CPU time (s) 138.33 Current children cumulated vsize (Kb) 82216 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 20896 0 2 0 14705 120 0 0 20 0 1 0 1841267041 85852160 20802 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 20960 20802 145 145 0 20815 0 [pid=19176] vsize: 83840 Current children cumulated CPU time (s) 148.25 Current children cumulated vsize (Kb) 85964 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 15693 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557285 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 158.18 Current children cumulated vsize (Kb) 89160 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 16693 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 168.18 Current children cumulated vsize (Kb) 89160 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 17693 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 178.18 Current children cumulated vsize (Kb) 89160 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 18694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 188.19 Current children cumulated vsize (Kb) 89160 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 19694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 198.19 Current children cumulated vsize (Kb) 89160 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 20694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 208.19 Current children cumulated vsize (Kb) 89160 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 21694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 218.19 Current children cumulated vsize (Kb) 89160 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 22694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 228.19 Current children cumulated vsize (Kb) 89160 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 23694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 238.19 Current children cumulated vsize (Kb) 89160 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 24695 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 248.2 Current children cumulated vsize (Kb) 89160 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 25694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 258.19 Current children cumulated vsize (Kb) 89160 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 26694 126 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 268.2 Current children cumulated vsize (Kb) 89160 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21691 0 2 0 27694 126 0 0 25 0 1 0 1841267041 89124864 21597 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21597 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 278.2 Current children cumulated vsize (Kb) 89160 [startup+290.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21692 0 2 0 28695 126 0 0 25 0 1 0 1841267041 89124864 21598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21598 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 288.21 Current children cumulated vsize (Kb) 89160 [startup+300.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21694 0 2 0 29695 126 0 0 25 0 1 0 1841267041 89124864 21600 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 21759 21600 145 145 0 21614 0 [pid=19176] vsize: 87036 Current children cumulated CPU time (s) 298.21 Current children cumulated vsize (Kb) 89160 [startup+310.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 22341 0 2 0 30687 129 0 0 25 0 1 0 1841267041 91774976 22247 4294967295 134512640 135094434 3221224432 3221223104 134556462 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 22406 22247 145 145 0 22261 0 [pid=19176] vsize: 89624 Current children cumulated CPU time (s) 308.16 Current children cumulated vsize (Kb) 91748 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23151 0 2 0 31672 135 0 0 25 0 1 0 1841267041 95137792 23057 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23227 23057 145 145 0 23082 0 [pid=19176] vsize: 92908 Current children cumulated CPU time (s) 318.07 Current children cumulated vsize (Kb) 95032 [startup+330.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23418 0 2 0 32668 137 0 0 25 0 1 0 1841267041 96223232 23324 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23324 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 328.05 Current children cumulated vsize (Kb) 96092 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23420 0 2 0 33668 137 0 0 25 0 1 0 1841267041 96223232 23326 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23326 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 338.05 Current children cumulated vsize (Kb) 96092 [startup+350.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23420 0 2 0 34669 137 0 0 25 0 1 0 1841267041 96223232 23326 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23326 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 348.06 Current children cumulated vsize (Kb) 96092 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23421 0 2 0 35669 137 0 0 25 0 1 0 1841267041 96223232 23327 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23327 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 358.06 Current children cumulated vsize (Kb) 96092 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 36669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 368.06 Current children cumulated vsize (Kb) 96092 [startup+380.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 37669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 378.06 Current children cumulated vsize (Kb) 96092 [startup+390.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 38669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 388.06 Current children cumulated vsize (Kb) 96092 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 39669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 398.06 Current children cumulated vsize (Kb) 96092 [startup+410.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 40670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 408.07 Current children cumulated vsize (Kb) 96092 [startup+420.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 41670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 418.07 Current children cumulated vsize (Kb) 96092 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 42670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 428.07 Current children cumulated vsize (Kb) 96092 [startup+440.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 43670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 438.07 Current children cumulated vsize (Kb) 96092 [startup+450.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 44670 138 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 448.08 Current children cumulated vsize (Kb) 96092 [startup+460.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 45670 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 458.08 Current children cumulated vsize (Kb) 96092 [startup+470.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 46670 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 468.08 Current children cumulated vsize (Kb) 96092 [startup+480.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 47670 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 478.08 Current children cumulated vsize (Kb) 96092 [startup+490.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 48671 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0 [pid=19176] vsize: 93968 Current children cumulated CPU time (s) 488.09 Current children cumulated vsize (Kb) 96092 [startup+500.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23821 0 2 0 49666 140 0 0 25 0 1 0 1841267041 97845248 23727 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 23888 23727 145 145 0 23743 0 [pid=19176] vsize: 95552 Current children cumulated CPU time (s) 498.06 Current children cumulated vsize (Kb) 97676 [startup+510.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 24767 0 2 0 50651 147 0 0 25 0 1 0 1841267041 101736448 24673 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 24838 24673 145 145 0 24693 0 [pid=19176] vsize: 99352 Current children cumulated CPU time (s) 507.98 Current children cumulated vsize (Kb) 101476 [startup+520.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 25724 0 2 0 51638 153 0 0 25 0 1 0 1841267041 105697280 25630 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 25805 25630 145 145 0 25660 0 [pid=19176] vsize: 103220 Current children cumulated CPU time (s) 517.91 Current children cumulated vsize (Kb) 105344 [startup+530.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 26489 0 2 0 52628 157 0 0 25 0 1 0 1841267041 108863488 26395 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 26578 26395 145 145 0 26433 0 [pid=19176] vsize: 106312 Current children cumulated CPU time (s) 527.85 Current children cumulated vsize (Kb) 108436 [startup+540.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 27370 0 2 0 53615 163 0 0 25 0 1 0 1841267041 112508928 27276 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 27468 27276 145 145 0 27323 0 [pid=19176] vsize: 109872 Current children cumulated CPU time (s) 537.78 Current children cumulated vsize (Kb) 111996 [startup+550.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 28158 0 2 0 54602 168 0 0 25 0 1 0 1841267041 115773440 28064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 28265 28064 145 145 0 28120 0 [pid=19176] vsize: 113060 Current children cumulated CPU time (s) 547.7 Current children cumulated vsize (Kb) 115184 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 28903 0 2 0 55591 174 0 0 25 0 1 0 1841267041 118841344 28809 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 29014 28809 145 145 0 28869 0 [pid=19176] vsize: 116056 Current children cumulated CPU time (s) 557.65 Current children cumulated vsize (Kb) 118180 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29472 0 2 0 56581 177 0 0 25 0 1 0 1841267041 121196544 29378 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 29589 29378 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 567.58 Current children cumulated vsize (Kb) 120480 [startup+580.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29473 0 2 0 57581 177 0 0 25 0 1 0 1841267041 121196544 29379 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19176/statm): 29589 29379 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 577.58 Current children cumulated vsize (Kb) 120480 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29478 0 2 0 58581 177 0 0 25 0 1 0 1841267041 121196544 29384 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29384 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 587.58 Current children cumulated vsize (Kb) 120480 [startup+600.047 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 59581 177 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 597.58 Current children cumulated vsize (Kb) 120480 [startup+610.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 60581 178 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 607.59 Current children cumulated vsize (Kb) 120480 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 61582 178 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 617.6 Current children cumulated vsize (Kb) 120480 [startup+630.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 62582 178 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 627.6 Current children cumulated vsize (Kb) 120480 [startup+640.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 63581 179 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 637.6 Current children cumulated vsize (Kb) 120480 [startup+650.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 64580 180 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 647.6 Current children cumulated vsize (Kb) 120480 [startup+660.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 65580 180 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 657.6 Current children cumulated vsize (Kb) 120480 [startup+670.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 66580 181 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 667.61 Current children cumulated vsize (Kb) 120480 [startup+680.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 67580 181 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 677.61 Current children cumulated vsize (Kb) 120480 [startup+690.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29486 0 2 0 68580 181 0 0 25 0 1 0 1841267041 121196544 29392 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29392 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 687.61 Current children cumulated vsize (Kb) 120480 [startup+700.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 69580 181 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223104 134556315 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 697.61 Current children cumulated vsize (Kb) 120480 [startup+710.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 70580 181 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 707.61 Current children cumulated vsize (Kb) 120480 [startup+720.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 71580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223024 134551897 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 717.62 Current children cumulated vsize (Kb) 120480 [startup+730.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 72580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 727.62 Current children cumulated vsize (Kb) 120480 [startup+740.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 73580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 737.62 Current children cumulated vsize (Kb) 120480 [startup+750.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 74580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 747.62 Current children cumulated vsize (Kb) 120480 [startup+760.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 75580 182 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 757.62 Current children cumulated vsize (Kb) 120480 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 76581 182 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 767.63 Current children cumulated vsize (Kb) 120480 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 77580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 777.63 Current children cumulated vsize (Kb) 120480 [startup+790.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 78580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 787.63 Current children cumulated vsize (Kb) 120480 [startup+800.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 79580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 797.63 Current children cumulated vsize (Kb) 120480 [startup+810.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 80581 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 807.64 Current children cumulated vsize (Kb) 120480 [startup+820.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 81580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 817.63 Current children cumulated vsize (Kb) 120480 [startup+830.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 82581 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 827.64 Current children cumulated vsize (Kb) 120480 [startup+840.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29492 0 2 0 83581 183 0 0 25 0 1 0 1841267041 121196544 29398 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29398 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 837.64 Current children cumulated vsize (Kb) 120480 [startup+850.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29493 0 2 0 84581 183 0 0 25 0 1 0 1841267041 121196544 29399 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29589 29399 145 145 0 29444 0 [pid=19176] vsize: 118356 Current children cumulated CPU time (s) 847.64 Current children cumulated vsize (Kb) 120480 [startup+860.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 85581 183 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 857.64 Current children cumulated vsize (Kb) 119928 [startup+870.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 86581 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 867.65 Current children cumulated vsize (Kb) 119928 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 87582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 877.66 Current children cumulated vsize (Kb) 119928 [startup+890.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 88582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 887.66 Current children cumulated vsize (Kb) 119928 [startup+900.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 89582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 897.66 Current children cumulated vsize (Kb) 119928 [startup+910.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 90582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 907.66 Current children cumulated vsize (Kb) 119928 [startup+920.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 91582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 917.66 Current children cumulated vsize (Kb) 119928 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 92583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 927.67 Current children cumulated vsize (Kb) 119928 [startup+940.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 93583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 937.67 Current children cumulated vsize (Kb) 119928 [startup+950.071 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 94583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 947.67 Current children cumulated vsize (Kb) 119928 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 95583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 957.67 Current children cumulated vsize (Kb) 119928 [startup+970.072 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 96584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 967.68 Current children cumulated vsize (Kb) 119928 [startup+980.073 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 97583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 977.67 Current children cumulated vsize (Kb) 119928 [startup+990.073 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 98584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 987.68 Current children cumulated vsize (Kb) 119928 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 99584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 997.68 Current children cumulated vsize (Kb) 119928 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 100584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1007.68 Current children cumulated vsize (Kb) 119928 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 101584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1017.68 Current children cumulated vsize (Kb) 119928 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 102585 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1027.69 Current children cumulated vsize (Kb) 119928 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 103585 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1037.69 Current children cumulated vsize (Kb) 119928 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 104585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1047.7 Current children cumulated vsize (Kb) 119928 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 105585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1057.7 Current children cumulated vsize (Kb) 119928 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 106585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1067.7 Current children cumulated vsize (Kb) 119928 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 107585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1077.7 Current children cumulated vsize (Kb) 119928 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 108586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1087.71 Current children cumulated vsize (Kb) 119928 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 109586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1097.71 Current children cumulated vsize (Kb) 119928 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 110586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1107.71 Current children cumulated vsize (Kb) 119928 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 111587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1117.72 Current children cumulated vsize (Kb) 119928 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 112586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1127.71 Current children cumulated vsize (Kb) 119928 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 113587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1137.72 Current children cumulated vsize (Kb) 119928 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 114587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1147.72 Current children cumulated vsize (Kb) 119928 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 115587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1157.72 Current children cumulated vsize (Kb) 119928 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 116587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1167.72 Current children cumulated vsize (Kb) 119928 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 117588 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1177.73 Current children cumulated vsize (Kb) 119928 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 118588 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1187.73 Current children cumulated vsize (Kb) 119928 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 119588 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1197.73 Current children cumulated vsize (Kb) 119928 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 120588 186 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1207.74 Current children cumulated vsize (Kb) 119928 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 19176 Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/19172/statm): 531 226 485 147 0 384 0 [pid=19172] vsize: 2124 Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 120588 186 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0 [pid=19176] vsize: 117804 Current children cumulated CPU time (s) 1207.74 Current children cumulated vsize (Kb) 119928 Sending SIGTERM to -19172 Sleeping 2 seconds One traced child (pid=19172) ended because it received signal 15 (SIGTERM) One traced child (pid=19176) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.15 CPU time (s): 1207.8 CPU user time (s): 1205.89 CPU system time (s): 1.91471 CPU usage (%): 99.806 Max. virtual memory (cumulated for all children) (Kb): 120480
ERROR: no interpretation found !