Name | submitted/aloul/FPGA_SAT05/normalized-fpga35_33_sat_pb.cnf.cr.opb |
MD5SUM | d4fd8917eebbcee2e1b2df9714e1fab8 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
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 | 36 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.58676 |
Number of variables | 1733 |
Total number of constraints | 1256 |
Number of constraints which are clauses | 1188 |
Number of constraints which are cardinality constraints (but not clauses) | 68 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 17 |
Maximum length of a constraint | 35 |
LAUNCH ON wulflinc17 THE 2005-09-18 12:33:19 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2389 boxname=wulflinc17 idbench=45 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d4fd8917eebbcee2e1b2df9714e1fab8 /oldhome/oroussel/tmp/wulflinc17/normalized-fpga35_33_sat_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-fpga35_33_sat_pb.cnf.cr.opb IDLAUNCH: 2389 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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: 984524 kB Buffers: 2468 kB Cached: 20892 kB SwapCached: 508 kB Active: 10744 kB Inactive: 14980 kB HighTotal: 131008 kB HighFree: 106204 kB LowTotal: 903652 kB LowFree: 878320 kB SwapTotal: 2097892 kB SwapFree: 2096672 kB Dirty: 44 kB Writeback: 0 kB Mapped: 5668 kB Slab: 18760 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 12:53:29 (client local time) WITH STATUS 0 IN 1209.24 SECONDS stats: 2389 7 1209.24 0
c Parsing PB file... c Converting 1256 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 67]---> BDD-cost: 63 c ---[ 66]---> BDD-cost: 63 c ---[ 65]---> BDD-cost: 63 c ---[ 64]---> BDD-cost: 63 c ---[ 63]---> BDD-cost: 63 c ---[ 62]---> BDD-cost: 63 c ---[ 61]---> BDD-cost: 63 c ---[ 60]---> BDD-cost: 63 c ---[ 59]---> BDD-cost: 63 c ---[ 58]---> BDD-cost: 63 c ---[ 57]---> BDD-cost: 63 c ---[ 56]---> BDD-cost: 63 c ---[ 55]---> BDD-cost: 63 c ---[ 54]---> BDD-cost: 63 c ---[ 53]---> BDD-cost: 63 c ---[ 52]---> BDD-cost: 63 c ---[ 51]---> BDD-cost: 63 c ---[ 50]---> BDD-cost: 63 c ---[ 49]---> BDD-cost: 63 c ---[ 48]---> BDD-cost: 63 c ---[ 47]---> BDD-cost: 63 c ---[ 46]---> BDD-cost: 63 c ---[ 45]---> BDD-cost: 63 c ---[ 44]---> BDD-cost: 63 c ---[ 43]---> BDD-cost: 63 c ---[ 42]---> BDD-cost: 63 c ---[ 41]---> BDD-cost: 63 c ---[ 40]---> BDD-cost: 63 c ---[ 39]---> BDD-cost: 63 c ---[ 38]---> BDD-cost: 63 c ---[ 37]---> BDD-cost: 63 c ---[ 36]---> BDD-cost: 63 c ---[ 35]---> BDD-cost: 63 c ---[ 34]---> BDD-cost: 63 c ---[ 33]---> BDD-cost: 63 c ---[ 32]---> BDD-cost: 31 c ---[ 31]---> BDD-cost: 31 c ---[ 30]---> BDD-cost: 31 c ---[ 29]---> BDD-cost: 31 c ---[ 28]---> BDD-cost: 31 c ---[ 27]---> BDD-cost: 31 c ---[ 26]---> BDD-cost: 31 c ---[ 25]---> BDD-cost: 31 c ---[ 24]---> BDD-cost: 31 c ---[ 23]---> BDD-cost: 31 c ---[ 22]---> BDD-cost: 31 c ---[ 21]---> BDD-cost: 31 c ---[ 20]---> BDD-cost: 31 c ---[ 19]---> BDD-cost: 31 c ---[ 18]---> BDD-cost: 31 c ---[ 17]---> BDD-cost: 31 c ---[ 16]---> BDD-cost: 33 c ---[ 15]---> BDD-cost: 33 c ---[ 14]---> BDD-cost: 33 c ---[ 13]---> BDD-cost: 33 c ---[ 12]---> BDD-cost: 33 c ---[ 11]---> BDD-cost: 33 c ---[ 10]---> BDD-cost: 33 c ---[ 9]---> BDD-cost: 33 c ---[ 8]---> BDD-cost: 33 c ---[ 7]---> BDD-cost: 33 c ---[ 6]---> BDD-cost: 33 c ---[ 5]---> BDD-cost: 33 c ---[ 4]---> BDD-cost: 33 c ---[ 3]---> BDD-cost: 33 c ---[ 2]---> BDD-cost: 33 c ---[ 1]---> BDD-cost: 33 c ---[ 0]---> BDD-cost: 33 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 9241 42349 | 3080 0 0 nan | 0.000 % | c | 100 | 9241 42349 | 3388 100 15655 156.6 | 1.361 % | c | 251 | 9241 42349 | 3726 251 45524 181.4 | 1.361 % | c | 477 | 9241 42349 | 4099 477 72619 152.2 | 1.361 % | c | 815 | 9241 42349 | 4509 815 137613 168.9 | 1.361 % | c | 1322 | 9241 42349 | 4960 1322 223413 169.0 | 1.361 % | c | 2081 | 9241 42349 | 5456 2081 293330 141.0 | 1.362 % | c | 3223 | 9241 42349 | 6002 3223 525259 163.0 | 1.361 % | c | 4931 | 9241 42349 | 6602 4931 873479 177.1 | 1.361 % | c | 7494 | 9241 42349 | 7262 7494 1597298 213.1 | 1.361 % | c | 11339 | 9241 42349 | 7988 7592 1338646 176.3 | 1.361 % | c | 17107 | 9241 42349 | 8787 7763 2704212 348.3 | 1.361 % | c | 25757 | 9241 42349 | 9666 10514 3001293 285.5 | 1.361 % | c | 38731 | 9241 42349 | 10632 11242 1345782 119.7 | 1.361 % | c | 58192 | 9241 42349 | 11696 11240 4033306 358.8 | 1.361 % | c | 87385 | 9241 42349 | 12865 9358 1029457 110.0 | 1.361 % | c | 131177 | 9241 42349 | 14152 14128 7100707 502.6 | 1.361 % | c | 196865 | 9241 42349 | 15567 17525 2100766 119.9 | 1.361 % | c | 295391 | 9241 42349 | 17124 17347 7062254 407.1 | 1.361 % | c | 443181 | 9241 42349 | 18836 11564 1917772 165.8 | 1.361 % |
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/23922/stat): 23922 (minisat+_script) R 23921 23922 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841310182 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/23922/statm): 174 3 169 147 0 27 0 [pid=23922] 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=23923 New process pid=23924 New process pid=23925 execve syscall for /bin/sed executable One traced child (pid=23924) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=23925) exited with status: 0 One traced child (pid=23923) exited with status: 0 New process pid=23926 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-fpga35_33_sat_pb.cnf.cr.opb [startup+10.0029 s] Raw data (loadavg): 0.61 0.85 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 2303 0 0 0 970 12 0 0 25 0 1 0 1841310187 9674752 2290 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 2362 2290 145 145 0 2217 0 [pid=23926] vsize: 9448 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 11572 [startup+20.0045 s] Raw data (loadavg): 0.67 0.85 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 3572 0 0 0 1955 18 0 0 25 0 1 0 1841310187 14888960 3559 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 3635 3559 145 145 0 3490 0 [pid=23926] vsize: 14540 Current children cumulated CPU time (s) 19.74 Current children cumulated vsize (Kb) 16664 [startup+30.0061 s] Raw data (loadavg): 0.72 0.85 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 4084 0 0 0 2949 21 0 0 25 0 1 0 1841310187 16990208 4071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 4148 4071 145 145 0 4003 0 [pid=23926] vsize: 16592 Current children cumulated CPU time (s) 29.71 Current children cumulated vsize (Kb) 18716 [startup+40.0068 s] Raw data (loadavg): 0.76 0.86 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 4696 0 0 0 3939 25 0 0 25 0 1 0 1841310187 19501056 4683 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 4761 4683 145 145 0 4616 0 [pid=23926] vsize: 19044 Current children cumulated CPU time (s) 39.65 Current children cumulated vsize (Kb) 21168 [startup+50.0084 s] Raw data (loadavg): 0.80 0.86 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 4696 0 0 0 4939 25 0 0 25 0 1 0 1841310187 19501056 4683 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 4761 4683 145 145 0 4616 0 [pid=23926] vsize: 19044 Current children cumulated CPU time (s) 49.65 Current children cumulated vsize (Kb) 21168 [startup+60.009 s] Raw data (loadavg): 0.83 0.87 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 4698 0 0 0 5938 26 0 0 25 0 1 0 1841310187 19501056 4685 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 4761 4685 145 145 0 4616 0 [pid=23926] vsize: 19044 Current children cumulated CPU time (s) 59.65 Current children cumulated vsize (Kb) 21168 [startup+70.0106 s] Raw data (loadavg): 0.85 0.87 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 4698 0 0 0 6938 26 0 0 25 0 1 0 1841310187 19501056 4685 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 4761 4685 145 145 0 4616 0 [pid=23926] vsize: 19044 Current children cumulated CPU time (s) 69.65 Current children cumulated vsize (Kb) 21168 [startup+80.0122 s] Raw data (loadavg): 0.88 0.87 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 5023 0 0 0 7932 29 0 0 25 0 1 0 1841310187 20832256 5010 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 5086 5010 145 145 0 4941 0 [pid=23926] vsize: 20344 Current children cumulated CPU time (s) 79.62 Current children cumulated vsize (Kb) 22468 [startup+90.0128 s] Raw data (loadavg): 0.89 0.88 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 5338 0 0 0 8928 31 0 0 25 0 1 0 1841310187 22147072 5325 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 5407 5325 145 145 0 5262 0 [pid=23926] vsize: 21628 Current children cumulated CPU time (s) 89.6 Current children cumulated vsize (Kb) 23752 [startup+100.013 s] Raw data (loadavg): 0.91 0.88 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 5359 0 0 0 9928 31 0 0 25 0 1 0 1841310187 22245376 5346 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 5431 5346 145 145 0 5286 0 [pid=23926] vsize: 21724 Current children cumulated CPU time (s) 99.6 Current children cumulated vsize (Kb) 23848 [startup+110.015 s] Raw data (loadavg): 0.92 0.89 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 5928 0 0 0 10916 36 0 0 25 0 1 0 1841310187 24596480 5915 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6005 5915 145 145 0 5860 0 [pid=23926] vsize: 24020 Current children cumulated CPU time (s) 109.53 Current children cumulated vsize (Kb) 26144 [startup+120.017 s] Raw data (loadavg): 0.93 0.89 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6445 0 0 0 11909 39 0 0 25 0 1 0 1841310187 26824704 6432 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6549 6432 145 145 0 6404 0 [pid=23926] vsize: 26196 Current children cumulated CPU time (s) 119.49 Current children cumulated vsize (Kb) 28320 [startup+130.017 s] Raw data (loadavg): 0.94 0.89 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6790 0 0 0 12903 42 0 0 25 0 1 0 1841310187 28291072 6777 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6777 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 129.46 Current children cumulated vsize (Kb) 29752 [startup+140.018 s] Raw data (loadavg): 0.95 0.89 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6791 0 0 0 13903 42 0 0 25 0 1 0 1841310187 28291072 6778 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6778 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 139.46 Current children cumulated vsize (Kb) 29752 [startup+150.019 s] Raw data (loadavg): 0.96 0.90 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6794 0 0 0 14903 43 0 0 25 0 1 0 1841310187 28291072 6781 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6781 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 149.47 Current children cumulated vsize (Kb) 29752 [startup+160.02 s] Raw data (loadavg): 0.96 0.90 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6795 0 0 0 15902 43 0 0 25 0 1 0 1841310187 28291072 6782 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6782 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 159.46 Current children cumulated vsize (Kb) 29752 [startup+170.022 s] Raw data (loadavg): 0.97 0.90 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6795 0 0 0 16902 44 0 0 25 0 1 0 1841310187 28291072 6782 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6782 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 169.47 Current children cumulated vsize (Kb) 29752 [startup+180.022 s] Raw data (loadavg): 0.97 0.91 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6795 0 0 0 17901 44 0 0 25 0 1 0 1841310187 28291072 6782 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6782 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 179.46 Current children cumulated vsize (Kb) 29752 [startup+190.023 s] Raw data (loadavg): 0.98 0.91 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6795 0 0 0 18899 46 0 0 25 0 1 0 1841310187 28291072 6782 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6782 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 189.46 Current children cumulated vsize (Kb) 29752 [startup+200.024 s] Raw data (loadavg): 0.98 0.91 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6795 0 0 0 19898 47 0 0 25 0 1 0 1841310187 28291072 6782 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6782 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 199.46 Current children cumulated vsize (Kb) 29752 [startup+210.025 s] Raw data (loadavg): 0.98 0.91 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6795 0 0 0 20898 48 0 0 25 0 1 0 1841310187 28291072 6782 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 6907 6782 145 145 0 6762 0 [pid=23926] vsize: 27628 Current children cumulated CPU time (s) 209.47 Current children cumulated vsize (Kb) 29752 [startup+220.027 s] Raw data (loadavg): 0.98 0.92 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6926 0 0 0 21894 49 0 0 25 0 1 0 1841310187 28827648 6913 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 7038 6913 145 145 0 6893 0 [pid=23926] vsize: 28152 Current children cumulated CPU time (s) 219.44 Current children cumulated vsize (Kb) 30276 [startup+230.028 s] Raw data (loadavg): 0.99 0.92 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 6926 0 0 0 22894 50 0 0 25 0 1 0 1841310187 28827648 6913 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 7038 6913 145 145 0 6893 0 [pid=23926] vsize: 28152 Current children cumulated CPU time (s) 229.45 Current children cumulated vsize (Kb) 30276 [startup+240.029 s] Raw data (loadavg): 0.99 0.92 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 7239 0 0 0 23888 53 0 0 25 0 1 0 1841310187 30113792 7226 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 7352 7226 145 145 0 7207 0 [pid=23926] vsize: 29408 Current children cumulated CPU time (s) 239.42 Current children cumulated vsize (Kb) 31532 [startup+250.029 s] Raw data (loadavg): 0.99 0.92 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 7418 0 0 0 24885 55 0 0 25 0 1 0 1841310187 30842880 7405 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 7530 7405 145 145 0 7385 0 [pid=23926] vsize: 30120 Current children cumulated CPU time (s) 249.41 Current children cumulated vsize (Kb) 32244 [startup+260.03 s] Raw data (loadavg): 0.99 0.92 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 7916 0 0 0 25877 58 0 0 25 0 1 0 1841310187 32882688 7903 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 8028 7903 145 145 0 7883 0 [pid=23926] vsize: 32112 Current children cumulated CPU time (s) 259.36 Current children cumulated vsize (Kb) 34236 [startup+270.031 s] Raw data (loadavg): 0.99 0.93 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 8569 0 0 0 26867 63 0 0 25 0 1 0 1841310187 35610624 8556 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 8694 8556 145 145 0 8549 0 [pid=23926] vsize: 34776 Current children cumulated CPU time (s) 269.31 Current children cumulated vsize (Kb) 36900 [startup+280.031 s] Raw data (loadavg): 0.99 0.93 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 8569 0 0 0 27866 63 0 0 25 0 1 0 1841310187 35610624 8556 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 8694 8556 145 145 0 8549 0 [pid=23926] vsize: 34776 Current children cumulated CPU time (s) 279.3 Current children cumulated vsize (Kb) 36900 [startup+290.032 s] Raw data (loadavg): 0.99 0.93 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9020 0 0 0 28860 66 0 0 25 0 1 0 1841310187 37498880 9007 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 9155 9007 145 145 0 9010 0 [pid=23926] vsize: 36620 Current children cumulated CPU time (s) 289.27 Current children cumulated vsize (Kb) 38744 [startup+300.032 s] Raw data (loadavg): 0.99 0.93 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9618 0 0 0 29853 69 0 0 25 0 1 0 1841310187 39948288 9605 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 9753 9605 145 145 0 9608 0 [pid=23926] vsize: 39012 Current children cumulated CPU time (s) 299.23 Current children cumulated vsize (Kb) 41136 [startup+310.033 s] Raw data (loadavg): 0.99 0.93 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9618 0 0 0 30853 69 0 0 25 0 1 0 1841310187 39948288 9605 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 9753 9605 145 145 0 9608 0 [pid=23926] vsize: 39012 Current children cumulated CPU time (s) 309.23 Current children cumulated vsize (Kb) 41136 [startup+320.034 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9618 0 0 0 31853 69 0 0 25 0 1 0 1841310187 39948288 9605 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 9753 9605 145 145 0 9608 0 [pid=23926] vsize: 39012 Current children cumulated CPU time (s) 319.23 Current children cumulated vsize (Kb) 41136 [startup+330.034 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 32848 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 329.21 Current children cumulated vsize (Kb) 42580 [startup+340.035 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 33848 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 339.21 Current children cumulated vsize (Kb) 42580 [startup+350.035 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 34849 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 349.22 Current children cumulated vsize (Kb) 42580 [startup+360.036 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 35849 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 359.22 Current children cumulated vsize (Kb) 42580 [startup+370.037 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 36849 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 369.22 Current children cumulated vsize (Kb) 42580 [startup+380.037 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 37849 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 379.22 Current children cumulated vsize (Kb) 42580 [startup+390.037 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 38850 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 389.23 Current children cumulated vsize (Kb) 42580 [startup+400.037 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 39850 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 399.23 Current children cumulated vsize (Kb) 42580 [startup+410.038 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 40850 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 409.23 Current children cumulated vsize (Kb) 42580 [startup+420.039 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 41850 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 419.23 Current children cumulated vsize (Kb) 42580 [startup+430.039 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 42850 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 429.23 Current children cumulated vsize (Kb) 42580 [startup+440.04 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 43851 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 439.24 Current children cumulated vsize (Kb) 42580 [startup+450.04 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 44851 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 449.24 Current children cumulated vsize (Kb) 42580 [startup+460.041 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 45851 72 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 459.24 Current children cumulated vsize (Kb) 42580 [startup+470.043 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 46850 73 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221222992 134550333 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 469.24 Current children cumulated vsize (Kb) 42580 [startup+480.043 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 47850 73 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 479.24 Current children cumulated vsize (Kb) 42580 [startup+490.044 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 48850 73 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223024 134557277 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 489.24 Current children cumulated vsize (Kb) 42580 [startup+500.046 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 9966 0 0 0 49849 73 0 0 25 0 1 0 1841310187 41426944 9953 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10114 9953 145 145 0 9969 0 [pid=23926] vsize: 40456 Current children cumulated CPU time (s) 499.23 Current children cumulated vsize (Kb) 42580 [startup+510.046 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 10078 0 0 0 50847 75 0 0 25 0 1 0 1841310187 41889792 10065 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10227 10065 145 145 0 10082 0 [pid=23926] vsize: 40908 Current children cumulated CPU time (s) 509.23 Current children cumulated vsize (Kb) 43032 [startup+520.048 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 10078 0 0 0 51847 75 0 0 25 0 1 0 1841310187 41889792 10065 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10227 10065 145 145 0 10082 0 [pid=23926] vsize: 40908 Current children cumulated CPU time (s) 519.23 Current children cumulated vsize (Kb) 43032 [startup+530.049 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 10078 0 0 0 52846 76 0 0 25 0 1 0 1841310187 41889792 10065 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10227 10065 145 145 0 10082 0 [pid=23926] vsize: 40908 Current children cumulated CPU time (s) 529.23 Current children cumulated vsize (Kb) 43032 [startup+540.05 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 10134 0 0 0 53845 76 0 0 25 0 1 0 1841310187 42143744 10121 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 10289 10121 145 145 0 10144 0 [pid=23926] vsize: 41156 Current children cumulated CPU time (s) 539.22 Current children cumulated vsize (Kb) 43280 [startup+550.052 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11089 0 0 0 54831 82 0 0 25 0 1 0 1841310187 46055424 11076 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11244 11076 145 145 0 11099 0 [pid=23926] vsize: 44976 Current children cumulated CPU time (s) 549.14 Current children cumulated vsize (Kb) 47100 [startup+560.052 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11145 0 0 0 55829 82 0 0 25 0 1 0 1841310187 46280704 11132 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11299 11132 145 145 0 11154 0 [pid=23926] vsize: 45196 Current children cumulated CPU time (s) 559.12 Current children cumulated vsize (Kb) 47320 [startup+570.054 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11145 0 0 0 56829 83 0 0 25 0 1 0 1841310187 46280704 11132 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11299 11132 145 145 0 11154 0 [pid=23926] vsize: 45196 Current children cumulated CPU time (s) 569.13 Current children cumulated vsize (Kb) 47320 [startup+580.054 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11145 0 0 0 57829 83 0 0 25 0 1 0 1841310187 46280704 11132 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11299 11132 145 145 0 11154 0 [pid=23926] vsize: 45196 Current children cumulated CPU time (s) 579.13 Current children cumulated vsize (Kb) 47320 [startup+590.055 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11235 0 0 0 58827 84 0 0 25 0 1 0 1841310187 46649344 11222 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11389 11222 145 145 0 11244 0 [pid=23926] vsize: 45556 Current children cumulated CPU time (s) 589.12 Current children cumulated vsize (Kb) 47680 [startup+600.056 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11235 0 0 0 59826 84 0 0 25 0 1 0 1841310187 46649344 11222 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11389 11222 145 145 0 11244 0 [pid=23926] vsize: 45556 Current children cumulated CPU time (s) 599.11 Current children cumulated vsize (Kb) 47680 [startup+610.056 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11235 0 0 0 60825 85 0 0 25 0 1 0 1841310187 46649344 11222 4294967295 134512640 135094434 3221224432 3221223024 134551711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11389 11222 145 145 0 11244 0 [pid=23926] vsize: 45556 Current children cumulated CPU time (s) 609.11 Current children cumulated vsize (Kb) 47680 [startup+620.058 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11235 0 0 0 61825 85 0 0 25 0 1 0 1841310187 46649344 11222 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11389 11222 145 145 0 11244 0 [pid=23926] vsize: 45556 Current children cumulated CPU time (s) 619.11 Current children cumulated vsize (Kb) 47680 [startup+630.059 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11410 0 0 0 62823 86 0 0 25 0 1 0 1841310187 47390720 11397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11570 11397 145 145 0 11425 0 [pid=23926] vsize: 46280 Current children cumulated CPU time (s) 629.1 Current children cumulated vsize (Kb) 48404 [startup+640.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11410 0 0 0 63823 86 0 0 25 0 1 0 1841310187 47390720 11397 4294967295 134512640 135094434 3221224432 3221223024 134557221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11570 11397 145 145 0 11425 0 [pid=23926] vsize: 46280 Current children cumulated CPU time (s) 639.1 Current children cumulated vsize (Kb) 48404 [startup+650.062 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11410 0 0 0 64823 86 0 0 25 0 1 0 1841310187 47390720 11397 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11570 11397 145 145 0 11425 0 [pid=23926] vsize: 46280 Current children cumulated CPU time (s) 649.1 Current children cumulated vsize (Kb) 48404 [startup+660.062 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11410 0 0 0 65822 87 0 0 25 0 1 0 1841310187 47390720 11397 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11570 11397 145 145 0 11425 0 [pid=23926] vsize: 46280 Current children cumulated CPU time (s) 659.1 Current children cumulated vsize (Kb) 48404 [startup+670.064 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11463 0 0 0 66822 87 0 0 25 0 1 0 1841310187 47607808 11450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11450 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 669.1 Current children cumulated vsize (Kb) 48616 [startup+680.064 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 67822 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 679.1 Current children cumulated vsize (Kb) 48616 [startup+690.065 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 68822 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 689.1 Current children cumulated vsize (Kb) 48616 [startup+700.066 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 69822 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 699.1 Current children cumulated vsize (Kb) 48616 [startup+710.066 s] Raw data (loadavg): 1.07 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 70823 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 709.11 Current children cumulated vsize (Kb) 48616 [startup+720.067 s] Raw data (loadavg): 1.06 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 71823 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 719.11 Current children cumulated vsize (Kb) 48616 [startup+730.067 s] Raw data (loadavg): 1.05 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 72823 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 729.11 Current children cumulated vsize (Kb) 48616 [startup+740.068 s] Raw data (loadavg): 1.04 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 73823 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223056 134562146 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 739.11 Current children cumulated vsize (Kb) 48616 [startup+750.07 s] Raw data (loadavg): 1.03 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 74824 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 749.12 Current children cumulated vsize (Kb) 48616 [startup+760.07 s] Raw data (loadavg): 1.03 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 75824 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 759.12 Current children cumulated vsize (Kb) 48616 [startup+770.072 s] Raw data (loadavg): 1.02 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 76824 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 769.12 Current children cumulated vsize (Kb) 48616 [startup+780.072 s] Raw data (loadavg): 1.02 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 77824 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 779.12 Current children cumulated vsize (Kb) 48616 [startup+790.073 s] Raw data (loadavg): 1.02 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 78824 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 789.12 Current children cumulated vsize (Kb) 48616 [startup+800.074 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 79825 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 799.13 Current children cumulated vsize (Kb) 48616 [startup+810.074 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 80825 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223104 134556533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 809.13 Current children cumulated vsize (Kb) 48616 [startup+820.076 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 81825 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 819.13 Current children cumulated vsize (Kb) 48616 [startup+830.076 s] Raw data (loadavg): 1.01 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 82825 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 829.13 Current children cumulated vsize (Kb) 48616 [startup+840.077 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 83826 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 839.14 Current children cumulated vsize (Kb) 48616 [startup+850.079 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 84826 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 849.14 Current children cumulated vsize (Kb) 48616 [startup+860.079 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 85826 87 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 859.14 Current children cumulated vsize (Kb) 48616 [startup+870.079 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11464 0 0 0 86826 88 0 0 25 0 1 0 1841310187 47607808 11451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23926/statm): 11623 11451 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 869.15 Current children cumulated vsize (Kb) 48616 [startup+880.079 s] Raw data (loadavg): 1.00 0.99 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11465 0 0 0 87825 88 0 0 25 0 1 0 1841310187 47607808 11452 4294967295 134512640 135094434 3221224432 3221223088 134556043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11452 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 879.14 Current children cumulated vsize (Kb) 48616 [startup+890.08 s] Raw data (loadavg): 1.08 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 88825 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 889.14 Current children cumulated vsize (Kb) 48616 [startup+900.081 s] Raw data (loadavg): 1.07 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 89825 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 899.14 Current children cumulated vsize (Kb) 48616 [startup+910.081 s] Raw data (loadavg): 1.06 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 90826 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 909.15 Current children cumulated vsize (Kb) 48616 [startup+920.082 s] Raw data (loadavg): 1.05 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 91826 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 919.15 Current children cumulated vsize (Kb) 48616 [startup+930.082 s] Raw data (loadavg): 1.04 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 92826 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 929.15 Current children cumulated vsize (Kb) 48616 [startup+940.083 s] Raw data (loadavg): 1.03 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 93826 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 939.15 Current children cumulated vsize (Kb) 48616 [startup+950.085 s] Raw data (loadavg): 1.03 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 94827 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 949.16 Current children cumulated vsize (Kb) 48616 [startup+960.085 s] Raw data (loadavg): 1.02 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 95827 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 959.16 Current children cumulated vsize (Kb) 48616 [startup+970.085 s] Raw data (loadavg): 1.02 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 96827 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 969.16 Current children cumulated vsize (Kb) 48616 [startup+980.085 s] Raw data (loadavg): 1.02 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 97827 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 979.16 Current children cumulated vsize (Kb) 48616 [startup+990.086 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 98827 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 989.16 Current children cumulated vsize (Kb) 48616 [startup+1000.09 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 99828 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 999.17 Current children cumulated vsize (Kb) 48616 [startup+1010.09 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 100828 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1009.17 Current children cumulated vsize (Kb) 48616 [startup+1020.09 s] Raw data (loadavg): 1.01 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 101828 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1019.17 Current children cumulated vsize (Kb) 48616 [startup+1030.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 102828 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1029.17 Current children cumulated vsize (Kb) 48616 [startup+1040.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 103829 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1039.18 Current children cumulated vsize (Kb) 48616 [startup+1050.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 104829 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1049.18 Current children cumulated vsize (Kb) 48616 [startup+1060.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 105829 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1059.18 Current children cumulated vsize (Kb) 48616 [startup+1070.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 106829 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1069.18 Current children cumulated vsize (Kb) 48616 [startup+1080.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 107830 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1079.19 Current children cumulated vsize (Kb) 48616 [startup+1090.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 108830 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1089.19 Current children cumulated vsize (Kb) 48616 [startup+1100.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 109830 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1099.19 Current children cumulated vsize (Kb) 48616 [startup+1110.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 110830 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1109.19 Current children cumulated vsize (Kb) 48616 [startup+1120.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 111830 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1119.19 Current children cumulated vsize (Kb) 48616 [startup+1130.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 112831 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1129.2 Current children cumulated vsize (Kb) 48616 [startup+1140.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 113831 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1139.2 Current children cumulated vsize (Kb) 48616 [startup+1150.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 114831 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1149.2 Current children cumulated vsize (Kb) 48616 [startup+1160.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 115831 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1159.2 Current children cumulated vsize (Kb) 48616 [startup+1170.09 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 116831 88 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1169.2 Current children cumulated vsize (Kb) 48616 [startup+1180.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 117831 89 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1179.21 Current children cumulated vsize (Kb) 48616 [startup+1190.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11467 0 0 0 118831 89 0 0 25 0 1 0 1841310187 47607808 11454 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11454 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1189.21 Current children cumulated vsize (Kb) 48616 [startup+1200.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11468 0 0 0 119831 89 0 0 25 0 1 0 1841310187 47607808 11455 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11455 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1199.21 Current children cumulated vsize (Kb) 48616 [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11468 0 0 0 120832 89 0 0 25 0 1 0 1841310187 47607808 11455 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11455 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1209.22 Current children cumulated vsize (Kb) 48616 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 0.95 2/57 23926 Raw data (/proc/23922/stat): 23922 (minisat+_script) S 23921 23922 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841310182 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/23922/statm): 531 226 485 147 0 384 0 [pid=23922] vsize: 2124 Raw data (/proc/23926/stat): 23926 (minisat+_64-bit) R 23922 23922 19316 0 -1 0 11468 0 0 0 120832 89 0 0 25 0 1 0 1841310187 47607808 11455 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23926/statm): 11623 11455 145 145 0 11478 0 [pid=23926] vsize: 46492 Current children cumulated CPU time (s) 1209.22 Current children cumulated vsize (Kb) 48616 Sending SIGTERM to -23922 Sleeping 2 seconds One traced child (pid=23922) ended because it received signal 15 (SIGTERM) One traced child (pid=23926) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.12 CPU time (s): 1209.24 CPU user time (s): 1208.32 CPU system time (s): 0.91586 CPU usage (%): 99.9268 Max. virtual memory (cumulated for all children) (Kb): 48616
ERROR: no interpretation found !