Name | submitted/aloul/FPGA_SAT05/normalized-chnl35_45_pb.cnf.cr.opb |
MD5SUM | 1f5fb3c191c2c77719f10f35e4f5f992 |
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 | 46 |
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.105983 |
Number of variables | 3150 |
Total number of constraints | 160 |
Number of constraints which are clauses | 90 |
Number of constraints which are cardinality constraints (but not clauses) | 70 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 35 |
Maximum length of a constraint | 45 |
LAUNCH ON wulflinc2 THE 2005-09-18 12:39:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2398 boxname=wulflinc2 idbench=54 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1f5fb3c191c2c77719f10f35e4f5f992 /oldhome/oroussel/tmp/wulflinc2/normalized-chnl35_45_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-chnl35_45_pb.cnf.cr.opb IDLAUNCH: 2398 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 948964 kB Buffers: 31812 kB Cached: 30388 kB SwapCached: 1040 kB Active: 19004 kB Inactive: 45856 kB HighTotal: 131008 kB HighFree: 97104 kB LowTotal: 903652 kB LowFree: 851860 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5696 kB Slab: 15076 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:59:30 (client local time) WITH STATUS 0 IN 1208.53 SECONDS stats: 2398 7 1208.53 0
c Parsing PB file... c Converting 160 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .......................................................................................... c ---[ 69]---> BDD-cost: 87 c ---[ 68]---> BDD-cost: 87 c ---[ 67]---> BDD-cost: 87 c ---[ 66]---> BDD-cost: 87 c ---[ 65]---> BDD-cost: 87 c ---[ 64]---> BDD-cost: 87 c ---[ 63]---> BDD-cost: 87 c ---[ 62]---> BDD-cost: 87 c ---[ 61]---> BDD-cost: 87 c ---[ 60]---> BDD-cost: 87 c ---[ 59]---> BDD-cost: 87 c ---[ 58]---> BDD-cost: 87 c ---[ 57]---> BDD-cost: 87 c ---[ 56]---> BDD-cost: 87 c ---[ 55]---> BDD-cost: 87 c ---[ 54]---> BDD-cost: 87 c ---[ 53]---> BDD-cost: 87 c ---[ 52]---> BDD-cost: 87 c ---[ 51]---> BDD-cost: 87 c ---[ 50]---> BDD-cost: 87 c ---[ 49]---> BDD-cost: 87 c ---[ 48]---> BDD-cost: 87 c ---[ 47]---> BDD-cost: 87 c ---[ 46]---> BDD-cost: 87 c ---[ 45]---> BDD-cost: 87 c ---[ 44]---> BDD-cost: 87 c ---[ 43]---> BDD-cost: 87 c ---[ 42]---> BDD-cost: 87 c ---[ 41]---> BDD-cost: 87 c ---[ 40]---> BDD-cost: 87 c ---[ 39]---> BDD-cost: 87 c ---[ 38]---> BDD-cost: 87 c ---[ 37]---> BDD-cost: 87 c ---[ 36]---> BDD-cost: 87 c ---[ 35]---> BDD-cost: 87 c ---[ 34]---> BDD-cost: 87 c ---[ 33]---> BDD-cost: 87 c ---[ 32]---> BDD-cost: 87 c ---[ 31]---> BDD-cost: 87 c ---[ 30]---> BDD-cost: 87 c ---[ 29]---> BDD-cost: 87 c ---[ 28]---> BDD-cost: 87 c ---[ 27]---> BDD-cost: 87 c ---[ 26]---> BDD-cost: 87 c ---[ 25]---> BDD-cost: 87 c ---[ 24]---> BDD-cost: 87 c ---[ 23]---> BDD-cost: 87 c ---[ 22]---> BDD-cost: 87 c ---[ 21]---> BDD-cost: 87 c ---[ 20]---> BDD-cost: 87 c ---[ 19]---> BDD-cost: 87 c ---[ 18]---> BDD-cost: 87 c ---[ 17]---> BDD-cost: 87 c ---[ 16]---> BDD-cost: 87 c ---[ 15]---> BDD-cost: 87 c ---[ 14]---> BDD-cost: 87 c ---[ 13]---> BDD-cost: 87 c ---[ 12]---> BDD-cost: 87 c ---[ 11]---> BDD-cost: 87 c ---[ 10]---> BDD-cost: 87 c ---[ 9]---> BDD-cost: 87 c ---[ 8]---> BDD-cost: 87 c ---[ 7]---> BDD-cost: 87 c ---[ 6]---> BDD-cost: 87 c ---[ 5]---> BDD-cost: 87 c ---[ 4]---> BDD-cost: 87 c ---[ 3]---> BDD-cost: 87 c ---[ 2]---> BDD-cost: 87 c ---[ 1]---> BDD-cost: 87 c ---[ 0]---> BDD-cost: 87 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 15210 42490 | 5070 0 0 nan | 0.000 % | c | 101 | 15210 42490 | 5577 101 13595 134.6 | 0.758 % | c | 253 | 15210 42490 | 6134 253 41155 162.7 | 0.758 % | c | 480 | 15210 42490 | 6748 480 87737 182.8 | 0.758 % | c | 819 | 15210 42490 | 7422 819 152105 185.7 | 0.758 % | c | 1328 | 15210 42490 | 8165 1328 233504 175.8 | 0.758 % | c | 2088 | 15210 42490 | 8981 2088 381775 182.8 | 0.758 % | c | 3227 | 15210 42490 | 9879 3227 722388 223.9 | 0.758 % | c | 4937 | 15210 42490 | 10867 4937 1190498 241.1 | 0.758 % | c | 7499 | 15210 42490 | 11954 7499 1875349 250.1 | 0.758 % | c | 11348 | 15210 42490 | 13150 11348 2998324 264.2 | 0.758 % | c | 17114 | 15210 42490 | 14465 8729 2872831 329.1 | 0.758 % | c | 25764 | 15210 42490 | 15911 17379 5578930 321.0 | 0.758 % | c | 38739 | 15210 42490 | 17503 11971 5497632 459.2 | 0.758 % | c | 58200 | 15210 42490 | 19253 10805 3533507 327.0 | 0.758 % | c | 87395 | 15210 42490 | 21178 25607 7805831 304.8 | 0.758 % | c | 131185 | 15210 42490 | 23296 15826 7858090 496.5 | 0.758 % | c | 196870 | 15210 42490 | 25626 23958 10195199 425.5 | 0.758 % |
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/9610/stat): 9610 (minisat+_script) R 9609 9610 6872 0 -1 0 18 0 1 0 0 0 0 0 21 0 1 0 1783106121 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9610/statm): 174 3 169 147 0 27 0 [pid=9610] 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=9611 New process pid=9612 New process pid=9613 execve syscall for /bin/sed executable 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 One traced child (pid=9612) exited with status: 0 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=9613) exited with status: 0 One traced child (pid=9611) exited with status: 0 New process pid=9614 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-chnl35_45_pb.cnf.cr.opb [startup+10.0205 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 2668 0 2 0 946 14 0 0 25 0 1 0 1783106131 11526144 2653 4294967295 134512640 135094434 3221224432 3221223024 134557396 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 2814 2653 145 145 0 2669 0 [pid=9614] vsize: 11256 Current children cumulated CPU time (s) 9.61 Current children cumulated vsize (Kb) 13380 [startup+20.0212 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) T 9610 9610 6872 0 -1 0 4463 0 2 0 1919 24 0 0 25 0 1 0 1783106131 18894848 4448 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9614/statm): 4613 4448 145 145 0 4468 0 [pid=9614] vsize: 18452 Current children cumulated CPU time (s) 19.44 Current children cumulated vsize (Kb) 20576 [startup+30.0229 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 5871 0 2 0 2897 34 0 0 25 0 1 0 1783106131 24649728 5856 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9614/statm): 6018 5856 145 145 0 5873 0 [pid=9614] vsize: 24072 Current children cumulated CPU time (s) 29.32 Current children cumulated vsize (Kb) 26196 [startup+40.0237 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6099 0 2 0 3892 37 0 0 25 0 1 0 1783106131 25649152 6084 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9614/statm): 6262 6084 145 145 0 6117 0 [pid=9614] vsize: 25048 Current children cumulated CPU time (s) 39.3 Current children cumulated vsize (Kb) 27172 [startup+50.0244 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6099 0 2 0 4891 37 0 0 25 0 1 0 1783106131 25649152 6084 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9614/statm): 6262 6084 145 145 0 6117 0 [pid=9614] vsize: 25048 Current children cumulated CPU time (s) 49.29 Current children cumulated vsize (Kb) 27172 [startup+60.0251 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6825 0 2 0 5880 40 0 0 25 0 1 0 1783106131 28643328 6810 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9614/statm): 6993 6810 145 145 0 6848 0 [pid=9614] vsize: 27972 Current children cumulated CPU time (s) 59.21 Current children cumulated vsize (Kb) 30096 [startup+70.0257 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6825 0 2 0 6880 40 0 0 25 0 1 0 1783106131 28643328 6810 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 6993 6810 145 145 0 6848 0 [pid=9614] vsize: 27972 Current children cumulated CPU time (s) 69.21 Current children cumulated vsize (Kb) 30096 [startup+80.0274 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 7243 0 2 0 7874 43 0 0 25 0 1 0 1783106131 30359552 7228 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 7412 7228 145 145 0 7267 0 [pid=9614] vsize: 29648 Current children cumulated CPU time (s) 79.18 Current children cumulated vsize (Kb) 31772 [startup+90.0281 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8225 0 2 0 8860 48 0 0 25 0 1 0 1783106131 34390016 8210 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 8396 8210 145 145 0 8251 0 [pid=9614] vsize: 33584 Current children cumulated CPU time (s) 89.09 Current children cumulated vsize (Kb) 35708 [startup+100.029 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8636 0 2 0 9855 50 0 0 25 0 1 0 1783106131 36085760 8621 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 8810 8621 145 145 0 8665 0 [pid=9614] vsize: 35240 Current children cumulated CPU time (s) 99.06 Current children cumulated vsize (Kb) 37364 [startup+110.031 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8636 0 2 0 10855 50 0 0 25 0 1 0 1783106131 36085760 8621 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 8810 8621 145 145 0 8665 0 [pid=9614] vsize: 35240 Current children cumulated CPU time (s) 109.06 Current children cumulated vsize (Kb) 37364 [startup+120.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8753 0 2 0 11854 51 0 0 25 0 1 0 1783106131 36573184 8738 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 8929 8738 145 145 0 8784 0 [pid=9614] vsize: 35716 Current children cumulated CPU time (s) 119.06 Current children cumulated vsize (Kb) 37840 [startup+130.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 9718 0 2 0 12839 57 0 0 25 0 1 0 1783106131 40525824 9703 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 9894 9703 145 145 0 9749 0 [pid=9614] vsize: 39576 Current children cumulated CPU time (s) 128.97 Current children cumulated vsize (Kb) 41700 [startup+140.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10177 0 2 0 13831 60 0 0 25 0 1 0 1783106131 42418176 10162 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10162 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 138.92 Current children cumulated vsize (Kb) 43548 [startup+150.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10179 0 2 0 14831 61 0 0 25 0 1 0 1783106131 42418176 10164 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10164 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 148.93 Current children cumulated vsize (Kb) 43548 [startup+160.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10180 0 2 0 15831 61 0 0 25 0 1 0 1783106131 42418176 10165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10165 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 158.93 Current children cumulated vsize (Kb) 43548 [startup+170.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 16831 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 168.93 Current children cumulated vsize (Kb) 43548 [startup+180.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 17831 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 178.93 Current children cumulated vsize (Kb) 43548 [startup+190.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 18832 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 188.94 Current children cumulated vsize (Kb) 43548 [startup+200.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 19832 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 198.94 Current children cumulated vsize (Kb) 43548 [startup+210.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10184 0 2 0 20832 61 0 0 25 0 1 0 1783106131 42418176 10169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10169 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 208.94 Current children cumulated vsize (Kb) 43548 [startup+220.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 21832 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 218.94 Current children cumulated vsize (Kb) 43548 [startup+230.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 22832 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 228.94 Current children cumulated vsize (Kb) 43548 [startup+240.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 23832 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 238.94 Current children cumulated vsize (Kb) 43548 [startup+250.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 24833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 248.95 Current children cumulated vsize (Kb) 43548 [startup+260.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 25833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 258.95 Current children cumulated vsize (Kb) 43548 [startup+270.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 26833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 268.95 Current children cumulated vsize (Kb) 43548 [startup+280.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 27833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 278.95 Current children cumulated vsize (Kb) 43548 [startup+290.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 28834 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0 [pid=9614] vsize: 41424 Current children cumulated CPU time (s) 288.96 Current children cumulated vsize (Kb) 43548 [startup+300.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10231 0 2 0 29833 61 0 0 25 0 1 0 1783106131 42602496 10216 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10401 10216 145 145 0 10256 0 [pid=9614] vsize: 41604 Current children cumulated CPU time (s) 298.95 Current children cumulated vsize (Kb) 43728 [startup+310.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10231 0 2 0 30833 62 0 0 25 0 1 0 1783106131 42602496 10216 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10401 10216 145 145 0 10256 0 [pid=9614] vsize: 41604 Current children cumulated CPU time (s) 308.96 Current children cumulated vsize (Kb) 43728 [startup+320.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10231 0 2 0 31833 62 0 0 25 0 1 0 1783106131 42602496 10216 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10401 10216 145 145 0 10256 0 [pid=9614] vsize: 41604 Current children cumulated CPU time (s) 318.96 Current children cumulated vsize (Kb) 43728 [startup+330.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10430 0 2 0 32830 63 0 0 25 0 1 0 1783106131 43417600 10415 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10600 10415 145 145 0 10455 0 [pid=9614] vsize: 42400 Current children cumulated CPU time (s) 328.94 Current children cumulated vsize (Kb) 44524 [startup+340.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 33828 65 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0 [pid=9614] vsize: 42728 Current children cumulated CPU time (s) 338.94 Current children cumulated vsize (Kb) 44852 [startup+350.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 34828 65 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0 [pid=9614] vsize: 42728 Current children cumulated CPU time (s) 348.94 Current children cumulated vsize (Kb) 44852 [startup+360.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 35828 66 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0 [pid=9614] vsize: 42728 Current children cumulated CPU time (s) 358.95 Current children cumulated vsize (Kb) 44852 [startup+370.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 36828 66 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0 [pid=9614] vsize: 42728 Current children cumulated CPU time (s) 368.95 Current children cumulated vsize (Kb) 44852 [startup+380.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10770 0 2 0 37823 68 0 0 25 0 1 0 1783106131 44814336 10755 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 10941 10755 145 145 0 10796 0 [pid=9614] vsize: 43764 Current children cumulated CPU time (s) 378.92 Current children cumulated vsize (Kb) 45888 [startup+390.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 11320 0 2 0 38813 72 0 0 25 0 1 0 1783106131 47095808 11305 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 11498 11305 145 145 0 11353 0 [pid=9614] vsize: 45992 Current children cumulated CPU time (s) 388.86 Current children cumulated vsize (Kb) 48116 [startup+400.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 11932 0 2 0 39803 76 0 0 25 0 1 0 1783106131 49610752 11917 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 12112 11917 145 145 0 11967 0 [pid=9614] vsize: 48448 Current children cumulated CPU time (s) 398.8 Current children cumulated vsize (Kb) 50572 [startup+410.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 12559 0 2 0 40793 81 0 0 25 0 1 0 1783106131 52178944 12544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 12739 12544 145 145 0 12594 0 [pid=9614] vsize: 50956 Current children cumulated CPU time (s) 408.75 Current children cumulated vsize (Kb) 53080 [startup+420.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 13116 0 2 0 41785 85 0 0 25 0 1 0 1783106131 54476800 13101 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 13300 13101 145 145 0 13155 0 [pid=9614] vsize: 53200 Current children cumulated CPU time (s) 418.71 Current children cumulated vsize (Kb) 55324 [startup+430.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 13718 0 2 0 42775 89 0 0 25 0 1 0 1783106131 56950784 13703 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 13904 13703 145 145 0 13759 0 [pid=9614] vsize: 55616 Current children cumulated CPU time (s) 428.65 Current children cumulated vsize (Kb) 57740 [startup+440.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14260 0 2 0 43765 93 0 0 25 0 1 0 1783106131 59195392 14245 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14452 14245 145 145 0 14307 0 [pid=9614] vsize: 57808 Current children cumulated CPU time (s) 438.59 Current children cumulated vsize (Kb) 59932 [startup+450.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14260 0 2 0 44765 93 0 0 25 0 1 0 1783106131 59195392 14245 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14452 14245 145 145 0 14307 0 [pid=9614] vsize: 57808 Current children cumulated CPU time (s) 448.59 Current children cumulated vsize (Kb) 59932 [startup+460.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14260 0 2 0 45766 93 0 0 25 0 1 0 1783106131 59195392 14245 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14452 14245 145 145 0 14307 0 [pid=9614] vsize: 57808 Current children cumulated CPU time (s) 458.6 Current children cumulated vsize (Kb) 59932 [startup+470.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14261 0 2 0 46766 93 0 0 25 0 1 0 1783106131 59195392 14246 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14452 14246 145 145 0 14307 0 [pid=9614] vsize: 57808 Current children cumulated CPU time (s) 468.6 Current children cumulated vsize (Kb) 59932 [startup+480.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14273 0 2 0 47766 93 0 0 25 0 1 0 1783106131 59260928 14258 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14468 14258 145 145 0 14323 0 [pid=9614] vsize: 57872 Current children cumulated CPU time (s) 478.6 Current children cumulated vsize (Kb) 59996 [startup+490.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14285 0 2 0 48766 93 0 0 25 0 1 0 1783106131 59326464 14270 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14484 14270 145 145 0 14339 0 [pid=9614] vsize: 57936 Current children cumulated CPU time (s) 488.6 Current children cumulated vsize (Kb) 60060 [startup+500.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14298 0 2 0 49766 93 0 0 25 0 1 0 1783106131 59392000 14283 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14500 14283 145 145 0 14355 0 [pid=9614] vsize: 58000 Current children cumulated CPU time (s) 498.6 Current children cumulated vsize (Kb) 60124 [startup+510.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14300 0 2 0 50766 93 0 0 25 0 1 0 1783106131 59392000 14285 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14500 14285 145 145 0 14355 0 [pid=9614] vsize: 58000 Current children cumulated CPU time (s) 508.6 Current children cumulated vsize (Kb) 60124 [startup+520.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14313 0 2 0 51766 94 0 0 25 0 1 0 1783106131 59457536 14298 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14516 14298 145 145 0 14371 0 [pid=9614] vsize: 58064 Current children cumulated CPU time (s) 518.61 Current children cumulated vsize (Kb) 60188 [startup+530.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14792 0 2 0 52758 97 0 0 25 0 1 0 1783106131 61415424 14777 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 14994 14777 145 145 0 14849 0 [pid=9614] vsize: 59976 Current children cumulated CPU time (s) 528.56 Current children cumulated vsize (Kb) 62100 [startup+540.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 15280 0 2 0 53750 101 0 0 25 0 1 0 1783106131 63418368 15265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 15483 15265 145 145 0 15338 0 [pid=9614] vsize: 61932 Current children cumulated CPU time (s) 538.52 Current children cumulated vsize (Kb) 64056 [startup+550.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 15802 0 2 0 54742 104 0 0 25 0 1 0 1783106131 65552384 15787 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 16004 15787 145 145 0 15859 0 [pid=9614] vsize: 64016 Current children cumulated CPU time (s) 548.47 Current children cumulated vsize (Kb) 66140 [startup+560.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16497 0 2 0 55731 108 0 0 25 0 1 0 1783106131 68403200 16482 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 16700 16482 145 145 0 16555 0 [pid=9614] vsize: 66800 Current children cumulated CPU time (s) 558.4 Current children cumulated vsize (Kb) 68924 [startup+570.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 56724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 568.36 Current children cumulated vsize (Kb) 70636 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 57724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223104 134555570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 578.36 Current children cumulated vsize (Kb) 70636 [startup+590.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 58724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 588.36 Current children cumulated vsize (Kb) 70636 [startup+600.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 59724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 598.36 Current children cumulated vsize (Kb) 70636 [startup+610.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 60724 111 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 608.36 Current children cumulated vsize (Kb) 70636 [startup+620.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 61724 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 618.37 Current children cumulated vsize (Kb) 70636 [startup+630.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 62725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 628.38 Current children cumulated vsize (Kb) 70636 [startup+640.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 63725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 638.38 Current children cumulated vsize (Kb) 70636 [startup+650.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 64725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 648.38 Current children cumulated vsize (Kb) 70636 [startup+660.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 65725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 658.38 Current children cumulated vsize (Kb) 70636 [startup+670.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 66726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 668.39 Current children cumulated vsize (Kb) 70636 [startup+680.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 67726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 678.39 Current children cumulated vsize (Kb) 70636 [startup+690.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 68726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 688.39 Current children cumulated vsize (Kb) 70636 [startup+700.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 69726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 698.39 Current children cumulated vsize (Kb) 70636 [startup+710.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 70726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 708.39 Current children cumulated vsize (Kb) 70636 [startup+720.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 71726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 718.39 Current children cumulated vsize (Kb) 70636 [startup+730.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 72727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 728.4 Current children cumulated vsize (Kb) 70636 [startup+740.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 73727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 738.4 Current children cumulated vsize (Kb) 70636 [startup+750.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 74727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 748.4 Current children cumulated vsize (Kb) 70636 [startup+760.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 75727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 758.4 Current children cumulated vsize (Kb) 70636 [startup+770.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 76727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 768.4 Current children cumulated vsize (Kb) 70636 [startup+780.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 77728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 778.41 Current children cumulated vsize (Kb) 70636 [startup+790.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 78728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 788.41 Current children cumulated vsize (Kb) 70636 [startup+800.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 79728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134551448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 798.41 Current children cumulated vsize (Kb) 70636 [startup+810.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 80728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 808.41 Current children cumulated vsize (Kb) 70636 [startup+820.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 81728 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 818.42 Current children cumulated vsize (Kb) 70636 [startup+830.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 82729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 828.43 Current children cumulated vsize (Kb) 70636 [startup+840.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 83729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 838.43 Current children cumulated vsize (Kb) 70636 [startup+850.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 84729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 848.43 Current children cumulated vsize (Kb) 70636 [startup+860.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 85729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 858.43 Current children cumulated vsize (Kb) 70636 [startup+870.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 86730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 868.44 Current children cumulated vsize (Kb) 70636 [startup+880.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 87730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 878.44 Current children cumulated vsize (Kb) 70636 [startup+890.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 88730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 888.44 Current children cumulated vsize (Kb) 70636 [startup+900.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 89730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 898.44 Current children cumulated vsize (Kb) 70636 [startup+910.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 90730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 908.44 Current children cumulated vsize (Kb) 70636 [startup+920.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16927 0 2 0 91730 113 0 0 25 0 1 0 1783106131 70156288 16912 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16912 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 918.44 Current children cumulated vsize (Kb) 70636 [startup+930.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16927 0 2 0 92730 113 0 0 25 0 1 0 1783106131 70156288 16912 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16912 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 928.44 Current children cumulated vsize (Kb) 70636 [startup+940.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16928 0 2 0 93729 114 0 0 25 0 1 0 1783106131 70156288 16913 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16913 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 938.44 Current children cumulated vsize (Kb) 70636 [startup+950.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16928 0 2 0 94728 115 0 0 25 0 1 0 1783106131 70156288 16913 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9614/statm): 17128 16913 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 948.44 Current children cumulated vsize (Kb) 70636 [startup+960.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 95727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 958.43 Current children cumulated vsize (Kb) 70636 [startup+970.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 96727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 968.43 Current children cumulated vsize (Kb) 70636 [startup+980.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 97727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 978.43 Current children cumulated vsize (Kb) 70636 [startup+990.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 98727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 988.43 Current children cumulated vsize (Kb) 70636 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 99727 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 998.44 Current children cumulated vsize (Kb) 70636 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 100727 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 1008.44 Current children cumulated vsize (Kb) 70636 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 101727 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 1018.44 Current children cumulated vsize (Kb) 70636 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 102728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 1028.45 Current children cumulated vsize (Kb) 70636 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 103728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 1038.45 Current children cumulated vsize (Kb) 70636 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 104728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 1048.45 Current children cumulated vsize (Kb) 70636 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 105728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 1058.45 Current children cumulated vsize (Kb) 70636 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 106728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0 [pid=9614] vsize: 68512 Current children cumulated CPU time (s) 1068.45 Current children cumulated vsize (Kb) 70636 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 107728 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1078.46 Current children cumulated vsize (Kb) 70436 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 108729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134556906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1088.47 Current children cumulated vsize (Kb) 70436 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 109729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1098.47 Current children cumulated vsize (Kb) 70436 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 110729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134551868 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1108.47 Current children cumulated vsize (Kb) 70436 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 111729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1118.47 Current children cumulated vsize (Kb) 70436 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 112729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1128.47 Current children cumulated vsize (Kb) 70436 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 113730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1138.48 Current children cumulated vsize (Kb) 70436 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 114730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223104 134556192 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1148.48 Current children cumulated vsize (Kb) 70436 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 115730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1158.48 Current children cumulated vsize (Kb) 70436 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 116730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1168.48 Current children cumulated vsize (Kb) 70436 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 117730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1178.48 Current children cumulated vsize (Kb) 70436 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 118730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1188.48 Current children cumulated vsize (Kb) 70436 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 119731 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223104 134556329 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1198.49 Current children cumulated vsize (Kb) 70436 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 120731 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1208.49 Current children cumulated vsize (Kb) 70436 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9614 Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9610/statm): 531 226 485 147 0 384 0 [pid=9610] vsize: 2124 Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 120731 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0 [pid=9614] vsize: 68312 Current children cumulated CPU time (s) 1208.49 Current children cumulated vsize (Kb) 70436 Sending SIGTERM to -9610 Sleeping 2 seconds One traced child (pid=9610) ended because it received signal 15 (SIGTERM) One traced child (pid=9614) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1208.53 CPU user time (s): 1207.32 CPU system time (s): 1.20982 CPU usage (%): 99.8667 Max. virtual memory (cumulated for all children) (Kb): 70636
ERROR: no interpretation found !