Name | submitted/aloul/FPGA_SAT05/normalized-chnl40_41_pb.cnf.cr.opb |
MD5SUM | 3c9e81ddaaf37dd621fe2bc839a3f27f |
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 | 42 |
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.107982 |
Number of variables | 3280 |
Total number of constraints | 162 |
Number of constraints which are clauses | 82 |
Number of constraints which are cardinality constraints (but not clauses) | 80 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 40 |
Maximum length of a constraint | 41 |
LAUNCH ON wulflinc5 THE 2005-09-18 12:25:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2358 boxname=wulflinc5 idbench=14 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3c9e81ddaaf37dd621fe2bc839a3f27f /oldhome/oroussel/tmp/wulflinc5/normalized-chnl40_41_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-chnl40_41_pb.cnf.cr.opb IDLAUNCH: 2358 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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 : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 948616 kB Buffers: 32144 kB Cached: 30248 kB SwapCached: 780 kB Active: 28260 kB Inactive: 36892 kB HighTotal: 131008 kB HighFree: 96572 kB LowTotal: 903652 kB LowFree: 852044 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5804 kB Slab: 15140 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:45:51 (client local time) WITH STATUS 0 IN 1208.71 SECONDS stats: 2358 7 1208.71 0
c Parsing PB file... c Converting 162 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................. c ---[ 79]---> BDD-cost: 79 c ---[ 78]---> BDD-cost: 79 c ---[ 77]---> BDD-cost: 79 c ---[ 76]---> BDD-cost: 79 c ---[ 75]---> BDD-cost: 79 c ---[ 74]---> BDD-cost: 79 c ---[ 73]---> BDD-cost: 79 c ---[ 72]---> BDD-cost: 79 c ---[ 71]---> BDD-cost: 79 c ---[ 70]---> BDD-cost: 79 c ---[ 69]---> BDD-cost: 79 c ---[ 68]---> BDD-cost: 79 c ---[ 67]---> BDD-cost: 79 c ---[ 66]---> BDD-cost: 79 c ---[ 65]---> BDD-cost: 79 c ---[ 64]---> BDD-cost: 79 c ---[ 63]---> BDD-cost: 79 c ---[ 62]---> BDD-cost: 79 c ---[ 61]---> BDD-cost: 79 c ---[ 60]---> BDD-cost: 79 c ---[ 59]---> BDD-cost: 79 c ---[ 58]---> BDD-cost: 79 c ---[ 57]---> BDD-cost: 79 c ---[ 56]---> BDD-cost: 79 c ---[ 55]---> BDD-cost: 79 c ---[ 54]---> BDD-cost: 79 c ---[ 53]---> BDD-cost: 79 c ---[ 52]---> BDD-cost: 79 c ---[ 51]---> BDD-cost: 79 c ---[ 50]---> BDD-cost: 79 c ---[ 49]---> BDD-cost: 79 c ---[ 48]---> BDD-cost: 79 c ---[ 47]---> BDD-cost: 79 c ---[ 46]---> BDD-cost: 79 c ---[ 45]---> BDD-cost: 79 c ---[ 44]---> BDD-cost: 79 c ---[ 43]---> BDD-cost: 79 c ---[ 42]---> BDD-cost: 79 c ---[ 41]---> BDD-cost: 79 c ---[ 40]---> BDD-cost: 79 c ---[ 39]---> BDD-cost: 79 c ---[ 38]---> BDD-cost: 79 c ---[ 37]---> BDD-cost: 79 c ---[ 36]---> BDD-cost: 79 c ---[ 35]---> BDD-cost: 79 c ---[ 34]---> BDD-cost: 79 c ---[ 33]---> BDD-cost: 79 c ---[ 32]---> BDD-cost: 79 c ---[ 31]---> BDD-cost: 79 c ---[ 30]---> BDD-cost: 79 c ---[ 29]---> BDD-cost: 79 c ---[ 28]---> BDD-cost: 79 c ---[ 27]---> BDD-cost: 79 c ---[ 26]---> BDD-cost: 79 c ---[ 25]---> BDD-cost: 79 c ---[ 24]---> BDD-cost: 79 c ---[ 23]---> BDD-cost: 79 c ---[ 22]---> BDD-cost: 79 c ---[ 21]---> BDD-cost: 79 c ---[ 20]---> BDD-cost: 79 c ---[ 19]---> BDD-cost: 79 c ---[ 18]---> BDD-cost: 79 c ---[ 17]---> BDD-cost: 79 c ---[ 16]---> BDD-cost: 79 c ---[ 15]---> BDD-cost: 79 c ---[ 14]---> BDD-cost: 79 c ---[ 13]---> BDD-cost: 79 c ---[ 12]---> BDD-cost: 79 c ---[ 11]---> BDD-cost: 79 c ---[ 10]---> BDD-cost: 79 c ---[ 9]---> BDD-cost: 79 c ---[ 8]---> BDD-cost: 79 c ---[ 7]---> BDD-cost: 79 c ---[ 6]---> BDD-cost: 79 c ---[ 5]---> BDD-cost: 79 c ---[ 4]---> BDD-cost: 79 c ---[ 3]---> BDD-cost: 79 c ---[ 2]---> BDD-cost: 79 c ---[ 1]---> BDD-cost: 79 c ---[ 0]---> BDD-cost: 79 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 15762 44080 | 5254 0 0 nan | 0.000 % | c | 101 | 15762 44080 | 5779 101 14280 141.4 | 0.833 % | c | 256 | 15762 44080 | 6357 256 40852 159.6 | 0.833 % | c | 482 | 15762 44080 | 6993 482 80226 166.4 | 0.833 % | c | 819 | 15762 44080 | 7692 819 132593 161.9 | 0.833 % | c | 1325 | 15762 44080 | 8461 1325 250938 189.4 | 0.833 % | c | 2086 | 15762 44080 | 9307 2086 455746 218.5 | 0.833 % | c | 3227 | 15762 44080 | 10238 3227 774769 240.1 | 0.833 % | c | 4940 | 15762 44080 | 11262 4940 1219231 246.8 | 0.833 % | c | 7503 | 15762 44080 | 12388 7503 1857014 247.5 | 0.833 % | c | 11351 | 15762 44080 | 13627 11351 3536314 311.5 | 0.833 % | c | 17117 | 15762 44080 | 14990 8595 3448950 401.3 | 0.833 % | c | 25767 | 15762 44080 | 16489 17245 7911433 458.8 | 0.833 % | c | 38741 | 15762 44080 | 18138 11355 3551431 312.8 | 0.833 % | c | 58203 | 15762 44080 | 19952 18809 7096779 377.3 | 0.833 % | c | 87395 | 15762 44080 | 21947 20922 8373757 400.2 | 0.833 % | c | 131188 | 15762 44080 | 24141 19495 9878054 506.7 | 0.833 % | c | 196873 | 15762 44080 | 26556 21140 8523475 403.2 | 0.833 % |
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/6857/stat): 6857 (minisat+_script) R 6856 6857 824 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1783017191 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/6857/statm): 174 3 169 147 0 27 0 [pid=6857] 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=6858 New process pid=6859 New process pid=6860 execve syscall for /bin/sed executable One traced child (pid=6859) 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=6860) exited with status: 0 One traced child (pid=6858) exited with status: 0 New process pid=6861 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-chnl40_41_pb.cnf.cr.opb [startup+10.0035 s] Raw data (loadavg): 0.84 0.69 0.82 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 2810 0 0 0 967 12 0 0 25 0 1 0 1783017196 12124160 2793 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 2960 2793 145 145 0 2815 0 [pid=6861] vsize: 11840 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 13964 [startup+20.0052 s] Raw data (loadavg): 0.87 0.70 0.82 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 4796 0 0 0 1943 21 0 0 25 0 1 0 1783017196 20271104 4779 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 4949 4779 145 145 0 4804 0 [pid=6861] vsize: 19796 Current children cumulated CPU time (s) 19.65 Current children cumulated vsize (Kb) 21920 [startup+30.0059 s] Raw data (loadavg): 0.89 0.71 0.82 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 6256 0 0 0 2921 31 0 0 25 0 1 0 1783017196 26238976 6239 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 6406 6239 145 145 0 6261 0 [pid=6861] vsize: 25624 Current children cumulated CPU time (s) 29.53 Current children cumulated vsize (Kb) 27748 [startup+40.0057 s] Raw data (loadavg): 0.90 0.72 0.82 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 6837 0 0 0 3913 34 0 0 25 0 1 0 1783017196 28684288 6820 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 7003 6820 145 145 0 6858 0 [pid=6861] vsize: 28012 Current children cumulated CPU time (s) 39.48 Current children cumulated vsize (Kb) 30136 [startup+50.0075 s] Raw data (loadavg): 0.92 0.73 0.82 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 7543 0 0 0 4903 39 0 0 25 0 1 0 1783017196 31576064 7526 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 7709 7526 145 145 0 7564 0 [pid=6861] vsize: 30836 Current children cumulated CPU time (s) 49.43 Current children cumulated vsize (Kb) 32960 [startup+60.0082 s] Raw data (loadavg): 0.93 0.73 0.82 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 8622 0 0 0 5886 47 0 0 25 0 1 0 1783017196 36016128 8605 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 8793 8605 145 145 0 8648 0 [pid=6861] vsize: 35172 Current children cumulated CPU time (s) 59.34 Current children cumulated vsize (Kb) 37296 [startup+70.0089 s] Raw data (loadavg): 0.94 0.74 0.82 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9192 0 0 0 6877 50 0 0 25 0 1 0 1783017196 38350848 9175 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 9363 9175 145 145 0 9218 0 [pid=6861] vsize: 37452 Current children cumulated CPU time (s) 69.28 Current children cumulated vsize (Kb) 39576 [startup+80.0107 s] Raw data (loadavg): 0.95 0.75 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9192 0 0 0 7876 50 0 0 25 0 1 0 1783017196 38350848 9175 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 9363 9175 145 145 0 9218 0 [pid=6861] vsize: 37452 Current children cumulated CPU time (s) 79.27 Current children cumulated vsize (Kb) 39576 [startup+90.0104 s] Raw data (loadavg): 0.96 0.76 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9192 0 0 0 8875 50 0 0 25 0 1 0 1783017196 38350848 9175 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9363 9175 145 145 0 9218 0 [pid=6861] vsize: 37452 Current children cumulated CPU time (s) 89.26 Current children cumulated vsize (Kb) 39576 [startup+100.011 s] Raw data (loadavg): 0.96 0.77 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9493 0 0 0 9870 52 0 0 25 0 1 0 1783017196 39600128 9476 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9668 9476 145 145 0 9523 0 [pid=6861] vsize: 38672 Current children cumulated CPU time (s) 99.23 Current children cumulated vsize (Kb) 40796 [startup+110.012 s] Raw data (loadavg): 0.97 0.77 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9669 0 0 0 10868 54 0 0 25 0 1 0 1783017196 40329216 9652 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9846 9652 145 145 0 9701 0 [pid=6861] vsize: 39384 Current children cumulated CPU time (s) 109.23 Current children cumulated vsize (Kb) 41508 [startup+120.013 s] Raw data (loadavg): 0.97 0.78 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9669 0 0 0 11868 54 0 0 25 0 1 0 1783017196 40329216 9652 4294967295 134512640 135094434 3221224432 3221222896 134780778 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9846 9652 145 145 0 9701 0 [pid=6861] vsize: 39384 Current children cumulated CPU time (s) 119.23 Current children cumulated vsize (Kb) 41508 [startup+130.013 s] Raw data (loadavg): 0.98 0.79 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9670 0 0 0 12869 54 0 0 25 0 1 0 1783017196 40329216 9653 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9846 9653 145 145 0 9701 0 [pid=6861] vsize: 39384 Current children cumulated CPU time (s) 129.24 Current children cumulated vsize (Kb) 41508 [startup+140.014 s] Raw data (loadavg): 0.98 0.79 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 13869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0 [pid=6861] vsize: 39384 Current children cumulated CPU time (s) 139.24 Current children cumulated vsize (Kb) 41508 [startup+150.015 s] Raw data (loadavg): 0.98 0.80 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 14869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0 [pid=6861] vsize: 39384 Current children cumulated CPU time (s) 149.24 Current children cumulated vsize (Kb) 41508 [startup+160.015 s] Raw data (loadavg): 0.98 0.81 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 15869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0 [pid=6861] vsize: 39384 Current children cumulated CPU time (s) 159.24 Current children cumulated vsize (Kb) 41508 [startup+170.015 s] Raw data (loadavg): 0.99 0.81 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 16869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0 [pid=6861] vsize: 39384 Current children cumulated CPU time (s) 169.24 Current children cumulated vsize (Kb) 41508 [startup+180.016 s] Raw data (loadavg): 0.99 0.82 0.83 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 10641 0 0 0 17855 60 0 0 25 0 1 0 1783017196 44302336 10624 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 10816 10624 145 145 0 10671 0 [pid=6861] vsize: 43264 Current children cumulated CPU time (s) 179.16 Current children cumulated vsize (Kb) 45388 [startup+190.016 s] Raw data (loadavg): 0.99 0.82 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11435 0 0 0 18844 65 0 0 25 0 1 0 1783017196 47558656 11418 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11611 11418 145 145 0 11466 0 [pid=6861] vsize: 46444 Current children cumulated CPU time (s) 189.1 Current children cumulated vsize (Kb) 48568 [startup+200.017 s] Raw data (loadavg): 0.99 0.83 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11437 0 0 0 19844 65 0 0 25 0 1 0 1783017196 47558656 11420 4294967295 134512640 135094434 3221224432 3221223024 134551906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11611 11420 145 145 0 11466 0 [pid=6861] vsize: 46444 Current children cumulated CPU time (s) 199.1 Current children cumulated vsize (Kb) 48568 [startup+210.017 s] Raw data (loadavg): 0.99 0.83 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11438 0 0 0 20844 65 0 0 25 0 1 0 1783017196 47558656 11421 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11611 11421 145 145 0 11466 0 [pid=6861] vsize: 46444 Current children cumulated CPU time (s) 209.1 Current children cumulated vsize (Kb) 48568 [startup+220.018 s] Raw data (loadavg): 0.99 0.84 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11438 0 0 0 21844 65 0 0 25 0 1 0 1783017196 47558656 11421 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11611 11421 145 145 0 11466 0 [pid=6861] vsize: 46444 Current children cumulated CPU time (s) 219.1 Current children cumulated vsize (Kb) 48568 [startup+230.019 s] Raw data (loadavg): 0.99 0.84 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11438 0 0 0 22845 65 0 0 25 0 1 0 1783017196 47558656 11421 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11611 11421 145 145 0 11466 0 [pid=6861] vsize: 46444 Current children cumulated CPU time (s) 229.11 Current children cumulated vsize (Kb) 48568 [startup+240.02 s] Raw data (loadavg): 0.99 0.85 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 23842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0 [pid=6861] vsize: 47200 Current children cumulated CPU time (s) 239.09 Current children cumulated vsize (Kb) 49324 [startup+250.02 s] Raw data (loadavg): 0.99 0.85 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 24842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0 [pid=6861] vsize: 47200 Current children cumulated CPU time (s) 249.09 Current children cumulated vsize (Kb) 49324 [startup+260.021 s] Raw data (loadavg): 0.99 0.86 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 25842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0 [pid=6861] vsize: 47200 Current children cumulated CPU time (s) 259.09 Current children cumulated vsize (Kb) 49324 [startup+270.022 s] Raw data (loadavg): 0.99 0.86 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 26842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0 [pid=6861] vsize: 47200 Current children cumulated CPU time (s) 269.09 Current children cumulated vsize (Kb) 49324 [startup+280.023 s] Raw data (loadavg): 0.99 0.86 0.84 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11729 0 0 0 27841 67 0 0 25 0 1 0 1783017196 48758784 11712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 11904 11712 145 145 0 11759 0 [pid=6861] vsize: 47616 Current children cumulated CPU time (s) 279.09 Current children cumulated vsize (Kb) 49740 [startup+290.023 s] Raw data (loadavg): 0.99 0.87 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 12269 0 0 0 28833 71 0 0 25 0 1 0 1783017196 50982912 12252 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 12447 12252 145 145 0 12302 0 [pid=6861] vsize: 49788 Current children cumulated CPU time (s) 289.05 Current children cumulated vsize (Kb) 51912 [startup+300.024 s] Raw data (loadavg): 0.99 0.87 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 12836 0 0 0 29823 75 0 0 25 0 1 0 1783017196 53313536 12819 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13016 12819 145 145 0 12871 0 [pid=6861] vsize: 52064 Current children cumulated CPU time (s) 298.99 Current children cumulated vsize (Kb) 54188 [startup+310.025 s] Raw data (loadavg): 0.99 0.88 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13066 0 0 0 30820 76 0 0 25 0 1 0 1783017196 54251520 13049 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13245 13049 145 145 0 13100 0 [pid=6861] vsize: 52980 Current children cumulated CPU time (s) 308.97 Current children cumulated vsize (Kb) 55104 [startup+320.026 s] Raw data (loadavg): 0.99 0.88 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13067 0 0 0 31820 76 0 0 25 0 1 0 1783017196 54251520 13050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13245 13050 145 145 0 13100 0 [pid=6861] vsize: 52980 Current children cumulated CPU time (s) 318.97 Current children cumulated vsize (Kb) 55104 [startup+330.027 s] Raw data (loadavg): 0.99 0.88 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13067 0 0 0 32820 76 0 0 25 0 1 0 1783017196 54251520 13050 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13245 13050 145 145 0 13100 0 [pid=6861] vsize: 52980 Current children cumulated CPU time (s) 328.97 Current children cumulated vsize (Kb) 55104 [startup+340.027 s] Raw data (loadavg): 0.99 0.89 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 33821 76 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0 [pid=6861] vsize: 52980 Current children cumulated CPU time (s) 338.98 Current children cumulated vsize (Kb) 55104 [startup+350.028 s] Raw data (loadavg): 0.99 0.89 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 34821 76 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223104 134556421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0 [pid=6861] vsize: 52980 Current children cumulated CPU time (s) 348.98 Current children cumulated vsize (Kb) 55104 [startup+360.028 s] Raw data (loadavg): 0.99 0.89 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 35821 76 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0 [pid=6861] vsize: 52980 Current children cumulated CPU time (s) 358.98 Current children cumulated vsize (Kb) 55104 [startup+370.029 s] Raw data (loadavg): 0.99 0.90 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 36821 77 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0 [pid=6861] vsize: 52980 Current children cumulated CPU time (s) 368.99 Current children cumulated vsize (Kb) 55104 [startup+380.03 s] Raw data (loadavg): 0.99 0.90 0.85 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 37820 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0 [pid=6861] vsize: 53404 Current children cumulated CPU time (s) 378.98 Current children cumulated vsize (Kb) 55528 [startup+390.03 s] Raw data (loadavg): 0.99 0.90 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 38820 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0 [pid=6861] vsize: 53404 Current children cumulated CPU time (s) 388.98 Current children cumulated vsize (Kb) 55528 [startup+400.03 s] Raw data (loadavg): 0.99 0.90 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 39821 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0 [pid=6861] vsize: 53404 Current children cumulated CPU time (s) 398.99 Current children cumulated vsize (Kb) 55528 [startup+410.031 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 40821 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0 [pid=6861] vsize: 53404 Current children cumulated CPU time (s) 408.99 Current children cumulated vsize (Kb) 55528 [startup+420.032 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 41821 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0 [pid=6861] vsize: 53404 Current children cumulated CPU time (s) 418.99 Current children cumulated vsize (Kb) 55528 [startup+430.033 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13879 0 0 0 42811 80 0 0 25 0 1 0 1783017196 57593856 13862 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 14061 13862 145 145 0 13916 0 [pid=6861] vsize: 56244 Current children cumulated CPU time (s) 428.92 Current children cumulated vsize (Kb) 58368 [startup+440.033 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14543 0 0 0 43798 86 0 0 25 0 1 0 1783017196 60305408 14526 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 14723 14526 145 145 0 14578 0 [pid=6861] vsize: 58892 Current children cumulated CPU time (s) 438.85 Current children cumulated vsize (Kb) 61016 [startup+450.034 s] Raw data (loadavg): 0.99 0.92 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 44795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0 [pid=6861] vsize: 59548 Current children cumulated CPU time (s) 448.83 Current children cumulated vsize (Kb) 61672 [startup+460.035 s] Raw data (loadavg): 0.99 0.92 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 45795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0 [pid=6861] vsize: 59548 Current children cumulated CPU time (s) 458.83 Current children cumulated vsize (Kb) 61672 [startup+470.036 s] Raw data (loadavg): 0.99 0.92 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 46795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0 [pid=6861] vsize: 59548 Current children cumulated CPU time (s) 468.83 Current children cumulated vsize (Kb) 61672 [startup+480.036 s] Raw data (loadavg): 0.99 0.92 0.86 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 47795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0 [pid=6861] vsize: 59548 Current children cumulated CPU time (s) 478.83 Current children cumulated vsize (Kb) 61672 [startup+490.037 s] Raw data (loadavg): 0.99 0.92 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 48794 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0 [pid=6861] vsize: 59548 Current children cumulated CPU time (s) 488.82 Current children cumulated vsize (Kb) 61672 [startup+500.039 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14830 0 0 0 49792 89 0 0 25 0 1 0 1783017196 61480960 14813 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 15010 14813 145 145 0 14865 0 [pid=6861] vsize: 60040 Current children cumulated CPU time (s) 498.82 Current children cumulated vsize (Kb) 62164 [startup+510.04 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 15919 0 0 0 50775 95 0 0 25 0 1 0 1783017196 65957888 15902 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 16103 15902 145 145 0 15958 0 [pid=6861] vsize: 64412 Current children cumulated CPU time (s) 508.71 Current children cumulated vsize (Kb) 66536 [startup+520.04 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 16804 0 0 0 51763 99 0 0 25 0 1 0 1783017196 69595136 16787 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 16991 16787 145 145 0 16846 0 [pid=6861] vsize: 67964 Current children cumulated CPU time (s) 518.63 Current children cumulated vsize (Kb) 70088 [startup+530.041 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17269 0 0 0 52755 103 0 0 25 0 1 0 1783017196 71503872 17252 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17252 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 528.59 Current children cumulated vsize (Kb) 71952 [startup+540.041 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17269 0 0 0 53755 103 0 0 25 0 1 0 1783017196 71503872 17252 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17252 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 538.59 Current children cumulated vsize (Kb) 71952 [startup+550.042 s] Raw data (loadavg): 0.99 0.94 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 54756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 548.6 Current children cumulated vsize (Kb) 71952 [startup+560.042 s] Raw data (loadavg): 0.99 0.94 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 55756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 558.6 Current children cumulated vsize (Kb) 71952 [startup+570.043 s] Raw data (loadavg): 0.99 0.94 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 56756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 568.6 Current children cumulated vsize (Kb) 71952 [startup+580.044 s] Raw data (loadavg): 0.99 0.94 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 57756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 578.6 Current children cumulated vsize (Kb) 71952 [startup+590.044 s] Raw data (loadavg): 0.99 0.94 0.87 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 58757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 588.61 Current children cumulated vsize (Kb) 71952 [startup+600.044 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 59757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 598.61 Current children cumulated vsize (Kb) 71952 [startup+610.045 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 60757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 608.61 Current children cumulated vsize (Kb) 71952 [startup+620.046 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 61757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0 [pid=6861] vsize: 69828 Current children cumulated CPU time (s) 618.61 Current children cumulated vsize (Kb) 71952 [startup+630.047 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 62754 105 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 628.6 Current children cumulated vsize (Kb) 72440 [startup+640.047 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 63754 106 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 638.61 Current children cumulated vsize (Kb) 72440 [startup+650.048 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 64754 106 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 648.61 Current children cumulated vsize (Kb) 72440 [startup+660.049 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 65754 106 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 658.61 Current children cumulated vsize (Kb) 72440 [startup+670.051 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 66754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 668.62 Current children cumulated vsize (Kb) 72440 [startup+680.051 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 67754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 678.62 Current children cumulated vsize (Kb) 72440 [startup+690.051 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 68754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 688.62 Current children cumulated vsize (Kb) 72440 [startup+700.052 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 69755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 698.63 Current children cumulated vsize (Kb) 72440 [startup+710.052 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 70754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 708.62 Current children cumulated vsize (Kb) 72440 [startup+720.053 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 71755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 718.63 Current children cumulated vsize (Kb) 72440 [startup+730.054 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 72755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 728.63 Current children cumulated vsize (Kb) 72440 [startup+740.055 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 73755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 738.63 Current children cumulated vsize (Kb) 72440 [startup+750.055 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 74755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 748.63 Current children cumulated vsize (Kb) 72440 [startup+760.056 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 75755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 758.63 Current children cumulated vsize (Kb) 72440 [startup+770.057 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 76755 108 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 768.64 Current children cumulated vsize (Kb) 72440 [startup+780.058 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 77756 108 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0 [pid=6861] vsize: 70316 Current children cumulated CPU time (s) 778.65 Current children cumulated vsize (Kb) 72440 [startup+790.058 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17575 0 0 0 78753 109 0 0 18 0 1 0 1783017196 72753152 17558 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 17762 17558 145 145 0 17617 0 [pid=6861] vsize: 71048 Current children cumulated CPU time (s) 788.63 Current children cumulated vsize (Kb) 73172 [startup+800.059 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17934 0 0 0 79747 112 0 0 25 0 1 0 1783017196 74248192 17917 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 18127 17917 145 145 0 17982 0 [pid=6861] vsize: 72508 Current children cumulated CPU time (s) 798.6 Current children cumulated vsize (Kb) 74632 [startup+810.06 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 80744 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 808.58 Current children cumulated vsize (Kb) 75280 [startup+820.062 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 81745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 818.59 Current children cumulated vsize (Kb) 75280 [startup+830.062 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 82745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 828.59 Current children cumulated vsize (Kb) 75280 [startup+840.063 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 83745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 838.59 Current children cumulated vsize (Kb) 75280 [startup+850.064 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 84745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 848.59 Current children cumulated vsize (Kb) 75280 [startup+860.065 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 85745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 858.59 Current children cumulated vsize (Kb) 75280 [startup+870.065 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 86746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 868.6 Current children cumulated vsize (Kb) 75280 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 87746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 878.6 Current children cumulated vsize (Kb) 75280 [startup+890.066 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 88746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 888.6 Current children cumulated vsize (Kb) 75280 [startup+900.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 89746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 898.6 Current children cumulated vsize (Kb) 75280 [startup+910.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 90746 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 908.61 Current children cumulated vsize (Kb) 75280 [startup+920.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 91747 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223104 134555553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 918.62 Current children cumulated vsize (Kb) 75280 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 92747 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 928.62 Current children cumulated vsize (Kb) 75280 [startup+940.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 93746 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 938.61 Current children cumulated vsize (Kb) 75280 [startup+950.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 94746 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223024 134551989 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 948.61 Current children cumulated vsize (Kb) 75280 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 95747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 958.62 Current children cumulated vsize (Kb) 75280 [startup+970.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 96747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 968.62 Current children cumulated vsize (Kb) 75280 [startup+980.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 97747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 978.62 Current children cumulated vsize (Kb) 75280 [startup+990.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 98747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 988.62 Current children cumulated vsize (Kb) 75280 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 99747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 998.62 Current children cumulated vsize (Kb) 75280 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 100748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1008.63 Current children cumulated vsize (Kb) 75280 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 101748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1018.63 Current children cumulated vsize (Kb) 75280 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 102748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1028.63 Current children cumulated vsize (Kb) 75280 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 103748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1038.63 Current children cumulated vsize (Kb) 75280 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 104748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1048.63 Current children cumulated vsize (Kb) 75280 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 105749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1058.64 Current children cumulated vsize (Kb) 75280 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 106749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1068.64 Current children cumulated vsize (Kb) 75280 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 107749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1078.64 Current children cumulated vsize (Kb) 75280 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 108749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1088.64 Current children cumulated vsize (Kb) 75280 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 109750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1098.65 Current children cumulated vsize (Kb) 75280 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 110750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1108.65 Current children cumulated vsize (Kb) 75280 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 111750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1118.65 Current children cumulated vsize (Kb) 75280 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 112750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1128.65 Current children cumulated vsize (Kb) 75280 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 113750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1138.65 Current children cumulated vsize (Kb) 75280 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 114751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1148.66 Current children cumulated vsize (Kb) 75280 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 115751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1158.66 Current children cumulated vsize (Kb) 75280 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 116751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1168.66 Current children cumulated vsize (Kb) 75280 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 117751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1178.66 Current children cumulated vsize (Kb) 75280 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 118752 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1188.67 Current children cumulated vsize (Kb) 75280 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 119752 115 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223104 134555768 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1198.68 Current children cumulated vsize (Kb) 75280 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 120752 115 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1208.68 Current children cumulated vsize (Kb) 75280 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6861 Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6857/statm): 531 226 485 147 0 384 0 [pid=6857] vsize: 2124 Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 120752 115 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0 [pid=6861] vsize: 73156 Current children cumulated CPU time (s) 1208.68 Current children cumulated vsize (Kb) 75280 Sending SIGTERM to -6857 Sleeping 2 seconds One traced child (pid=6857) ended because it received signal 15 (SIGTERM) One traced child (pid=6861) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1208.71 CPU user time (s): 1207.53 CPU system time (s): 1.18582 CPU usage (%): 99.8828 Max. virtual memory (cumulated for all children) (Kb): 75280
ERROR: no interpretation found !