| Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-10teams.opb |
| MD5SUM | 130bea0863cb3f92addf09aabe15daa3 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 956 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 1800 |
| Biggest coefficient in the objective function | 86 |
| Number of bits for the biggest coefficient in the objective function | 7 |
| Sum of the numbers in the objective function | 41700 |
| Number of bits of the sum of numbers in the objective function | 16 |
| Biggest number in a constraint | 86 |
| Number of bits of the biggest number in a constraint | 7 |
| Biggest sum of numbers in a constraint | 41700 |
| Number of bits of the biggest sum of numbers | 16 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1189.03 |
| Number of variables | 1800 |
| Total number of constraints | 2015 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 2015 |
| Number of constraints which are nor clauses,nor cardinality constraints | 0 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 72 |
LAUNCH ON wulflinc21 THE 2005-09-20 04:41:18 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3398 boxname=wulflinc21 idbench=1054 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 130bea0863cb3f92addf09aabe15daa3 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-10teams.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-10teams.opb IDLAUNCH: 3398 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 824200 kB Buffers: 32548 kB Cached: 148044 kB SwapCached: 832 kB Active: 64760 kB Inactive: 118484 kB HighTotal: 131008 kB HighFree: 21672 kB LowTotal: 903652 kB LowFree: 802528 kB SwapTotal: 2097892 kB SwapFree: 2096456 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5776 kB Slab: 21672 kB Committed_AS: 64368 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:01:29 (client local time) WITH STATUS 10 IN 1206.08 SECONDS stats: 3398 7 1206.08 10
c Parsing PB file... c Converting 330 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################################################## c -- Clauses(.)/Splits(s): (none) c ---[ 328]---> BDD-cost: 77 c ---[ 326]---> BDD-cost: 77 c ---[ 324]---> BDD-cost: 77 c ---[ 322]---> BDD-cost: 77 c ---[ 320]---> BDD-cost: 77 c ---[ 318]---> BDD-cost: 77 c ---[ 316]---> BDD-cost: 77 c ---[ 314]---> BDD-cost: 77 c ---[ 312]---> BDD-cost: 77 c ---[ 310]---> BDD-cost: 77 c ---[ 308]---> BDD-cost: 77 c ---[ 306]---> BDD-cost: 77 c ---[ 304]---> BDD-cost: 77 c ---[ 302]---> BDD-cost: 77 c ---[ 300]---> BDD-cost: 77 c ---[ 298]---> BDD-cost: 77 c ---[ 296]---> BDD-cost: 77 c ---[ 294]---> BDD-cost: 77 c ---[ 292]---> BDD-cost: 77 c ---[ 290]---> BDD-cost: 77 c ---[ 288]---> BDD-cost: 77 c ---[ 286]---> BDD-cost: 77 c ---[ 284]---> BDD-cost: 77 c ---[ 282]---> BDD-cost: 77 c ---[ 280]---> BDD-cost: 77 c ---[ 278]---> BDD-cost: 77 c ---[ 276]---> BDD-cost: 77 c ---[ 274]---> BDD-cost: 77 c ---[ 272]---> BDD-cost: 77 c ---[ 270]---> BDD-cost: 77 c ---[ 268]---> BDD-cost: 77 c ---[ 266]---> BDD-cost: 77 c ---[ 264]---> BDD-cost: 77 c ---[ 262]---> BDD-cost: 77 c ---[ 260]---> BDD-cost: 77 c ---[ 258]---> BDD-cost: 77 c ---[ 256]---> BDD-cost: 77 c ---[ 254]---> BDD-cost: 77 c ---[ 252]---> BDD-cost: 77 c ---[ 250]---> BDD-cost: 77 c ---[ 249]---> BDD-cost: 125 c ---[ 248]---> BDD-cost: 185 c ---[ 247]---> BDD-cost: 185 c ---[ 246]---> BDD-cost: 185 c ---[ 245]---> BDD-cost: 185 c ---[ 244]---> BDD-cost: 185 c ---[ 243]---> BDD-cost: 125 c ---[ 242]---> BDD-cost: 185 c ---[ 241]---> BDD-cost: 185 c ---[ 240]---> BDD-cost: 185 c ---[ 239]---> BDD-cost: 185 c ---[ 238]---> BDD-cost: 125 c ---[ 237]---> BDD-cost: 185 c ---[ 236]---> BDD-cost: 185 c ---[ 235]---> BDD-cost: 185 c ---[ 234]---> BDD-cost: 185 c ---[ 233]---> BDD-cost: 185 c ---[ 232]---> BDD-cost: 125 c ---[ 231]---> BDD-cost: 185 c ---[ 230]---> BDD-cost: 185 c ---[ 229]---> BDD-cost: 185 c ---[ 228]---> BDD-cost: 185 c ---[ 227]---> BDD-cost: 125 c ---[ 226]---> BDD-cost: 185 c ---[ 225]---> BDD-cost: 185 c ---[ 224]---> BDD-cost: 185 c ---[ 223]---> BDD-cost: 185 c ---[ 222]---> BDD-cost: 185 c ---[ 221]---> BDD-cost: 125 c ---[ 220]---> BDD-cost: 185 c ---[ 219]---> BDD-cost: 185 c ---[ 218]---> BDD-cost: 185 c ---[ 217]---> BDD-cost: 185 c ---[ 216]---> BDD-cost: 125 c ---[ 215]---> BDD-cost: 185 c ---[ 214]---> BDD-cost: 185 c ---[ 213]---> BDD-cost: 185 c ---[ 212]---> BDD-cost: 185 c ---[ 211]---> BDD-cost: 185 c ---[ 210]---> BDD-cost: 125 c ---[ 209]---> BDD-cost: 125 c ---[ 208]---> BDD-cost: 185 c ---[ 207]---> BDD-cost: 185 c ---[ 206]---> BDD-cost: 185 c ---[ 205]---> BDD-cost: 185 c ---[ 204]---> BDD-cost: 185 c ---[ 203]---> BDD-cost: 185 c ---[ 202]---> BDD-cost: 185 c ---[ 201]---> BDD-cost: 185 c ---[ 200]---> BDD-cost: 125 c ---[ 199]---> BDD-cost: 75 c ---[ 198]---> BDD-cost: 77 c ---[ 197]---> BDD-cost: 77 c ---[ 196]---> BDD-cost: 77 c ---[ 195]---> BDD-cost: 77 c ---[ 194]---> BDD-cost: 77 c ---[ 193]---> BDD-cost: 77 c ---[ 192]---> BDD-cost: 77 c ---[ 191]---> BDD-cost: 75 c ---[ 190]---> BDD-cost: 77 c ---[ 189]---> BDD-cost: 77 c ---[ 188]---> BDD-cost: 77 c ---[ 187]---> BDD-cost: 77 c ---[ 186]---> BDD-cost: 77 c ---[ 185]---> BDD-cost: 77 c ---[ 184]---> BDD-cost: 77 c ---[ 183]---> BDD-cost: 75 c ---[ 182]---> BDD-cost: 77 c ---[ 181]---> BDD-cost: 77 c ---[ 180]---> BDD-cost: 77 c ---[ 179]---> BDD-cost: 77 c ---[ 178]---> BDD-cost: 77 c ---[ 177]---> BDD-cost: 77 c ---[ 176]---> BDD-cost: 77 c ---[ 175]---> BDD-cost: 75 c ---[ 174]---> BDD-cost: 77 c ---[ 173]---> BDD-cost: 77 c ---[ 172]---> BDD-cost: 77 c ---[ 171]---> BDD-cost: 77 c ---[ 170]---> BDD-cost: 77 c ---[ 169]---> BDD-cost: 77 c ---[ 168]---> BDD-cost: 77 c ---[ 167]---> BDD-cost: 75 c ---[ 166]---> BDD-cost: 77 c ---[ 165]---> BDD-cost: 77 c ---[ 164]---> BDD-cost: 77 c ---[ 163]---> BDD-cost: 77 c ---[ 162]---> BDD-cost: 77 c ---[ 161]---> BDD-cost: 77 c ---[ 160]---> BDD-cost: 77 c ---[ 158]---> BDD-cost: 70 c ---[ 156]---> BDD-cost: 77 c ---[ 154]---> BDD-cost: 77 c ---[ 152]---> BDD-cost: 77 c ---[ 150]---> BDD-cost: 77 c ---[ 148]---> BDD-cost: 77 c ---[ 146]---> BDD-cost: 77 c ---[ 144]---> BDD-cost: 77 c ---[ 142]---> BDD-cost: 70 c ---[ 140]---> BDD-cost: 76 c ---[ 138]---> BDD-cost: 76 c ---[ 136]---> BDD-cost: 76 c ---[ 134]---> BDD-cost: 76 c ---[ 132]---> BDD-cost: 76 c ---[ 130]---> BDD-cost: 76 c ---[ 128]---> BDD-cost: 76 c ---[ 126]---> BDD-cost: 70 c ---[ 124]---> BDD-cost: 77 c ---[ 122]---> BDD-cost: 77 c ---[ 120]---> BDD-cost: 77 c ---[ 118]---> BDD-cost: 77 c ---[ 116]---> BDD-cost: 77 c ---[ 114]---> BDD-cost: 77 c ---[ 112]---> BDD-cost: 77 c ---[ 110]---> BDD-cost: 70 c ---[ 108]---> BDD-cost: 77 c ---[ 106]---> BDD-cost: 77 c ---[ 104]---> BDD-cost: 77 c ---[ 102]---> BDD-cost: 77 c ---[ 100]---> BDD-cost: 77 c ---[ 98]---> BDD-cost: 77 c ---[ 96]---> BDD-cost: 77 c ---[ 94]---> BDD-cost: 70 c ---[ 92]---> BDD-cost: 77 c ---[ 90]---> BDD-cost: 77 c ---[ 88]---> BDD-cost: 77 c ---[ 86]---> BDD-cost: 77 c ---[ 84]---> BDD-cost: 77 c ---[ 82]---> BDD-cost: 77 c ---[ 80]---> BDD-cost: 77 c ---[ 78]---> BDD-cost: 70 c ---[ 76]---> BDD-cost: 77 c ---[ 74]---> BDD-cost: 77 c ---[ 72]---> BDD-cost: 77 c ---[ 70]---> BDD-cost: 77 c ---[ 68]---> BDD-cost: 77 c ---[ 66]---> BDD-cost: 77 c ---[ 64]---> BDD-cost: 77 c ---[ 62]---> BDD-cost: 70 c ---[ 60]---> BDD-cost: 77 c ---[ 58]---> BDD-cost: 77 c ---[ 56]---> BDD-cost: 77 c ---[ 54]---> BDD-cost: 77 c ---[ 52]---> BDD-cost: 77 c ---[ 50]---> BDD-cost: 77 c ---[ 48]---> BDD-cost: 77 c ---[ 46]---> BDD-cost: 70 c ---[ 44]---> BDD-cost: 77 c ---[ 42]---> BDD-cost: 77 c ---[ 40]---> BDD-cost: 77 c ---[ 38]---> BDD-cost: 77 c ---[ 36]---> BDD-cost: 77 c ---[ 34]---> BDD-cost: 77 c ---[ 32]---> BDD-cost: 77 c ---[ 30]---> BDD-cost: 70 c ---[ 28]---> BDD-cost: 77 c ---[ 26]---> BDD-cost: 77 c ---[ 24]---> BDD-cost: 77 c ---[ 22]---> BDD-cost: 77 c ---[ 20]---> BDD-cost: 77 c ---[ 18]---> BDD-cost: 77 c ---[ 16]---> BDD-cost: 77 c ---[ 14]---> BDD-cost: 70 c ---[ 12]---> BDD-cost: 77 c ---[ 10]---> BDD-cost: 77 c ---[ 8]---> BDD-cost: 77 c ---[ 6]---> BDD-cost: 77 c ---[ 4]---> BDD-cost: 77 c ---[ 2]---> BDD-cost: 77 c ---[ 0]---> BDD-cost: 77 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 53221 141547 | 17740 0 0 nan | 0.000 % | c | 100 | 53221 141547 | 19514 100 818 8.2 | 1.808 % | c | 250 | 53221 141547 | 21465 250 15400 61.6 | 1.808 % | c | 475 | 53221 141547 | 23611 475 28793 60.6 | 1.808 % | c | 812 | 53221 141547 | 25973 812 62995 77.6 | 1.808 % | c | 1318 | 53221 141547 | 28570 1318 139369 105.7 | 1.808 % | c | 2077 | 53221 141547 | 31427 2077 324252 156.1 | 1.808 % | c | 3216 | 53221 141547 | 34570 3216 511801 159.1 | 1.808 % | c ============================================================================== c [1mFound solution: 968[0m c ---[ 0]---> Adder-cost: 7750 maxlim: 39032 bits: 16/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4874 | 107351 334867 | 35783 4874 723583 148.5 | 1.808 % | c | 4974 | 107351 334867 | 39361 4974 725539 145.9 | 1.399 % | c | 5125 | 107351 334867 | 43297 5125 734785 143.4 | 1.399 % | c | 5350 | 107351 334867 | 47627 5350 757972 141.7 | 1.399 % | c | 5687 | 107351 334867 | 52389 5687 805904 141.7 | 1.399 % | c | 6194 | 107351 334867 | 57628 6194 880515 142.2 | 1.399 % | c | 6954 | 107351 334867 | 63391 6954 975482 140.3 | 1.399 % | c | 8095 | 107351 334867 | 69730 8095 1140642 140.9 | 1.399 % | c | 9805 | 107351 334867 | 76704 9805 1611033 164.3 | 1.399 % | c | 12371 | 107351 334867 | 84374 12371 2352458 190.2 | 1.399 % | c ============================================================================== c [1mFound solution: 962[0m c ---[ 0]---> Adder-cost: 0 maxlim: 39038 bits: 16/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14541 | 107358 334912 | 35786 14541 2732241 187.9 | 1.399 % | c | 14642 | 107358 334912 | 39364 14642 2734861 186.8 | 1.409 % | c | 14794 | 107358 334912 | 43301 14794 2754967 186.2 | 1.409 % | c | 15020 | 107358 334912 | 47631 15020 2763373 184.0 | 1.409 % | c | 15357 | 107358 334912 | 52394 15357 2798874 182.3 | 1.409 % | c | 15864 | 107358 334912 | 57633 15864 2845711 179.4 | 1.409 % | c | 16623 | 107358 334912 | 63397 16623 2939938 176.9 | 1.409 % | c | 17762 | 107358 334912 | 69736 17762 3170459 178.5 | 1.409 % | c | 19470 | 107358 334912 | 76710 19470 3736178 191.9 | 1.409 % | c | 22034 | 107358 334912 | 84381 22034 4404757 199.9 | 1.409 % | c | 25881 | 107358 334912 | 92819 25881 5484850 211.9 | 1.409 % | c | 31647 | 107358 334912 | 102101 31647 7222673 228.2 | 1.409 % | c | 40297 | 107358 334912 | 112311 40297 9703101 240.8 | 1.409 % | c | 53271 | 107358 334912 | 123542 53271 13645727 256.2 | 1.409 % | c | 72733 | 107358 334912 | 135897 72733 21970585 302.1 | 1.409 % | c | 101925 | 107350 334882 | 149487 101924 33904393 332.6 | 1.412 % | c c *** TERMINATED *** s SATISFIABLE v -x10212_bit0 -x10312_bit0 -x20312_bit0 -x10412_bit0 -x20412_bit0 -x30412_bit0 -x10512_bit0 -x20512_bit0 -x30512_bit0 -x40512_bit0 x10612_bit0 -x20612_bit0 -x30612_bit0 -x40612_bit0 -x50612_bit0 -x10712_bit0 -x20712_bit0 -x30712_bit0 -x40712_bit0 -x50712_bit0 -x60712_bit0 -x10812_bit0 -x20812_bit0 -x30812_bit0 -x40812_bit0 -x50812_bit0 -x60812_bit0 -x70812_bit0 -x10912_bit0 -x20912_bit0 -x30912_bit0 -x40912_bit0 -x50912_bit0 -x60912_bit0 -x70912_bit0 -x80912_bit0 -x11012_bit0 -x21012_bit0 -x31012_bit0 -x41012_bit0 -x51012_bit0 -x61012_bit0 -x71012_bit0 -x81012_bit0 -x91012_bit0 -x10222_bit0 -x10322_bit0 -x20322_bit0 -x10422_bit0 -x20422_bit0 -x30422_bit0 -x10522_bit0 -x20522_bit0 -x30522_bit0 -x40522_bit0 -x10622_bit0 -x20622_bit0 -x30622_bit0 -x40622_bit0 -x50622_bit0 -x10722_bit0 -x20722_bit0 -x30722_bit0 -x40722_bit0 -x50722_bit0 -x60722_bit0 -x10822_bit0 -x20822_bit0 -x30822_bit0 -x40822_bit0 -x50822_bit0 -x60822_bit0 -x70822_bit0 -x10922_bit0 -x20922_bit0 -x30922_bit0 -x40922_bit0 -x50922_bit0 -x60922_bit0 -x70922_bit0 -x80922_bit0 -x11022_bit0 -x21022_bit0 -x31022_bit0 -x41022_bit0 x51022_bit0 -x61022_bit0 -x71022_bit0 -x81022_bit0 -x91022_bit0 -x10232_bit0 -x10332_bit0 -x20332_bit0 -x10432_bit0 -x20432_bit0 -x30432_bit0 -x10532_bit0 -x20532_bit0 -x30532_bit0 -x40532_bit0 -x10632_bit0 -x20632_bit0 -x30632_bit0 -x40632_bit0 -x50632_bit0 -x10732_bit0 -x20732_bit0 x30732_bit0 -x40732_bit0 -x50732_bit0 -x60732_bit0 -x10832_bit0 -x20832_bit0 -x30832_bit0 -x40832_bit0 -x50832_bit0 -x60832_bit0 -x70832_bit0 -x10932_bit0 -x20932_bit0 -x30932_bit0 -x40932_bit0 -x50932_bit0 -x60932_bit0 -x70932_bit0 -x80932_bit0 -x11032_bit0 -x21032_bit0 -x31032_bit0 -x41032_bit0 -x51032_bit0 -x61032_bit0 -x71032_bit0 -x81032_bit0 -x91032_bit0 -x10242_bit0 -x10342_bit0 -x20342_bit0 -x10442_bit0 -x20442_bit0 -x30442_bit0 -x10542_bit0 -x20542_bit0 -x30542_bit0 -x40542_bit0 -x10642_bit0 -x20642_bit0 -x30642_bit0 -x40642_bit0 -x50642_bit0 -x10742_bit0 -x20742_bit0 -x30742_bit0 -x40742_bit0 -x50742_bit0 -x60742_bit0 -x10842_bit0 -x20842_bit0 -x30842_bit0 -x40842_bit0 -x50842_bit0 -x60842_bit0 -x70842_bit0 -x10942_bit0 x20942_bit0 -x30942_bit0 -x40942_bit0 -x50942_bit0 -x60942_bit0 -x70942_bit0 -x80942_bit0 -x11042_bit0 -x21042_bit0 -x31042_bit0 -x41042_bit0 -x51042_bit0 -x61042_bit0 -x71042_bit0 -x81042_bit0 -x91042_bit0 -x10252_bit0 -x10352_bit0 -x20352_bit0 -x10452_bit0 -x20452_bit0 -x30452_bit0 -x10552_bit0 -x20552_bit0 -x30552_bit0 -x40552_bit0 -x10652_bit0 -x20652_bit0 -x30652_bit0 -x40652_bit0 -x50652_bit0 -x10752_bit0 -x20752_bit0 -x30752_bit0 -x40752_bit0 -x50752_bit0 -x60752_bit0 -x10852_bit0 -x20852_bit0 -x30852_bit0 x40852_bit0 -x50852_bit0 -x60852_bit0 -x70852_bit0 -x10952_bit0 -x20952_bit0 -x30952_bit0 -x40952_bit0 -x50952_bit0 -x60952_bit0 -x70952_bit0 -x80952_bit0 -x11052_bit0 -x21052_bit0 -x31052_bit0 -x41052_bit0 -x51052_bit0 -x61052_bit0 -x71052_bit0 -x81052_bit0 -x91052_bit0 -x10213_bit0 -x10313_bit0 -x20313_bit0 -x10413_bit0 -x20413_bit0 -x30413_bit0 -x10513_bit0 -x20513_bit0 -x30513_bit0 -x40513_bit0 -x10613_bit0 -x20613_bit0 -x30613_bit0 -x40613_bit0 -x50613_bit0 -x10713_bit0 -x20713_bit0 -x30713_bit0 -x40713_bit0 -x50713_bit0 -x60713_bit0 -x10813_bit0 -x20813_bit0 -x30813_bit0 -x40813_bit0 -x50813_bit0 -x60813_bit0 -x70813_bit0 -x10913_bit0 -x20913_bit0 -x30913_bit0 -x40913_bit0 -x50913_bit0 -x60913_bit0 -x70913_bit0 x80913_bit0 -x11013_bit0 -x21013_bit0 -x31013_bit0 -x41013_bit0 -x51013_bit0 -x61013_bit0 -x71013_bit0 -x81013_bit0 -x91013_bit0 -x10223_bit0 -x10323_bit0 -x20323_bit0 -x10423_bit0 -x20423_bit0 -x30423_bit0 x10523_bit0 -x20523_bit0 -x30523_bit0 -x40523_bit0 -x10623_bit0 -x20623_bit0 -x30623_bit0 -x40623_bit0 -x50623_bit0 -x10723_bit0 -x20723_bit0 -x30723_bit0 -x40723_bit0 -x50723_bit0 -x60723_bit0 -x10823_bit0 -x20823_bit0 -x30823_bit0 -x40823_bit0 -x50823_bit0 -x60823_bit0 -x70823_bit0 -x10923_bit0 -x20923_bit0 -x30923_bit0 -x40923_bit0 -x50923_bit0 -x60923_bit0 -x70923_bit0 -x80923_bit0 -x11023_bit0 -x21023_bit0 -x31023_bit0 -x41023_bit0 -x51023_bit0 -x61023_bit0 -x71023_bit0 -x81023_bit0 -x91023_bit0 -x10233_bit0 -x10333_bit0 -x20333_bit0 -x10433_bit0 -x20433_bit0 -x30433_bit0 -x10533_bit0 -x20533_bit0 -x30533_bit0 -x40533_bit0 -x10633_bit0 -x20633_bit0 -x30633_bit0 -x40633_bit0 -x50633_bit0 -x10733_bit0 x20733_bit0 -x30733_bit0 -x40733_bit0 -x50733_bit0 -x60733_bit0 -x10833_bit0 -x20833_bit0 -x30833_bit0 -x40833_bit0 -x50833_bit0 -x60833_bit0 -x70833_bit0 -x10933_bit0 -x20933_bit0 -x30933_bit0 -x40933_bit0 -x50933_bit0 -x60933_bit0 -x70933_bit0 -x80933_bit0 -x11033_bit0 -x21033_bit0 -x31033_bit0 -x41033_bit0 -x51033_bit0 -x61033_bit0 -x71033_bit0 -x81033_bit0 -x91033_bit0 -x10243_bit0 -x10343_bit0 -x20343_bit0 -x10443_bit0 -x20443_bit0 -x30443_bit0 -x10543_bit0 -x20543_bit0 -x30543_bit0 -x40543_bit0 -x10643_bit0 -x20643_bit0 -x30643_bit0 -x40643_bit0 -x50643_bit0 -x10743_bit0 -x20743_bit0 -x30743_bit0 -x40743_bit0 -x50743_bit0 -x60743_bit0 -x10843_bit0 -x20843_bit0 -x30843_bit0 -x40843_bit0 -x50843_bit0 -x60843_bit0 -x70843_bit0 -x10943_bit0 -x20943_bit0 -x30943_bit0 -x40943_bit0 -x50943_bit0 -x60943_bit0 -x70943_bit0 -x80943_bit0 -x11043_bit0 -x21043_bit0 -x31043_bit0 x41043_bit0 -x51043_bit0 -x61043_bit0 -x71043_bit0 -x81043_bit0 -x91043_bit0 -x10253_bit0 -x10353_bit0 -x20353_bit0 -x10453_bit0 -x20453_bit0 -x30453_bit0 -x10553_bit0 -x20553_bit0 -x30553_bit0 -x40553_bit0 -x10653_bit0 -x20653_bit0 x30653_bit0 -x40653_bit0 -x50653_bit0 -x10753_bit0 -x20753_bit0 -x30753_bit0 -x40753_bit0 -x50753_bit0 -x60753_bit0 -x10853_bit0 -x20853_bit0 -x30853_bit0 -x40853_bit0 -x50853_bit0 -x60853_bit0 -x70853_bit0 -x10953_bit0 -x20953_bit0 -x30953_bit0 -x40953_bit0 -x50953_bit0 -x60953_bit0 -x70953_bit0 -x80953_bit0 -x11053_bit0 -x21053_bit0 -x31053_bit0 -x41053_bit0 -x51053_bit0 -x61053_bit0 -x71053_bit0 -x81053_bit0 -x91053_bit0 -x10214_bit0 -x10314_bit0 x20314_bit0 -x10414_bit0 -x20414_bit0 -x30414_bit0 -x10514_bit0 -x20514_bit0 -x30514_bit0 -x40514_bit0 -x10614_bit0 -x20614_bit0 -x30614_bit0 -x40614_bit0 -x50614_bit0 -x10714_bit0 -x20714_bit0 -x30714_bit0 -x40714_bit0 -x50714_bit0 -x60714_bit0 -x10814_bit0 -x20814_bit0 -x30814_bit0 -x40814_bit0 -x50814_bit0 -x60814_bit0 -x70814_bit0 -x10914_bit0 -x20914_bit0 -x30914_bit0 -x40914_bit0 -x50914_bit0 -x60914_bit0 -x70914_bit0 -x80914_bit0 -x11014_bit0 -x21014_bit0 -x31014_bit0 -x41014_bit0 -x51014_bit0 -x61014_bit0 -x71014_bit0 -x81014_bit0 -x91014_bit0 -x10224_bit0 -x10324_bit0 -x20324_bit0 -x10424_bit0 -x20424_bit0 -x30424_bit0 -x10524_bit0 -x20524_bit0 -x30524_bit0 -x40524_bit0 -x10624_bit0 -x20624_bit0 -x30624_bit0 -x40624_bit0 -x50624_bit0 x10724_bit0 -x20724_bit0 -x30724_bit0 -x40724_bit0 -x50724_bit0 -x60724_bit0 -x10824_bit0 -x20824_bit0 -x30824_bit0 -x40824_bit0 -x50824_bit0 -x60824_bit0 -x70824_bit0 -x10924_bit0 -x20924_bit0 -x30924_bit0 -x40924_bit0 -x50924_bit0 -x60924_bit0 -x70924_bit0 -x80924_bit0 -x11024_bit0 -x21024_bit0 -x31024_bit0 -x41024_bit0 -x51024_bit0 -x61024_bit0 -x71024_bit0 -x81024_bit0 -x91024_bit0 -x10234_bit0 -x10334_bit0 -x20334_bit0 -x10434_bit0 -x20434_bit0 -x30434_bit0 -x10534_bit0 -x20534_bit0 -x30534_bit0 -x40534_bit0 -x10634_bit0 -x20634_bit0 -x30634_bit0 -x40634_bit0 -x50634_bit0 -x10734_bit0 -x20734_bit0 -x30734_bit0 -x40734_bit0 -x50734_bit0 -x60734_bit0 -x10834_bit0 -x20834_bit0 -x30834_bit0 -x40834_bit0 -x50834_bit0 -x60834_bit0 -x70834_bit0 -x10934_bit0 -x20934_bit0 -x30934_bit0 x40934_bit0 -x50934_bit0 -x60934_bit0 -x70934_bit0 -x80934_bit0 -x11034_bit0 -x21034_bit0 -x31034_bit0 -x41034_bit0 -x51034_bit0 -x61034_bit0 -x71034_bit0 -x81034_bit0 -x91034_bit0 -x10244_bit0 -x10344_bit0 -x20344_bit0 -x10444_bit0 -x20444_bit0 -x30444_bit0 -x10544_bit0 -x20544_bit0 -x30544_bit0 -x40544_bit0 -x10644_bit0 -x20644_bit0 -x30644_bit0 -x40644_bit0 -x50644_bit0 -x10744_bit0 -x20744_bit0 -x30744_bit0 -x40744_bit0 -x50744_bit0 -x60744_bit0 -x10844_bit0 -x20844_bit0 -x30844_bit0 -x40844_bit0 x50844_bit0 -x60844_bit0 -x70844_bit0 -x10944_bit0 -x20944_bit0 -x30944_bit0 -x40944_bit0 -x50944_bit0 -x60944_bit0 -x70944_bit0 -x80944_bit0 -x11044_bit0 -x21044_bit0 -x31044_bit0 -x41044_bit0 -x51044_bit0 -x61044_bit0 -x71044_bit0 -x81044_bit0 -x91044_bit0 -x10254_bit0 -x10354_bit0 -x20354_bit0 -x10454_bit0 -x20454_bit0 -x30454_bit0 -x10554_bit0 -x20554_bit0 -x30554_bit0 -x40554_bit0 -x10654_bit0 -x20654_bit0 -x30654_bit0 -x40654_bit0 -x50654_bit0 -x10754_bit0 -x20754_bit0 -x30754_bit0 -x40754_bit0 -x50754_bit0 -x60754_bit0 -x10854_bit0 -x20854_bit0 -x30854_bit0 -x40854_bit0 -x50854_bit0 -x60854_bit0 -x70854_bit0 -x10954_bit0 -x20954_bit0 -x30954_bit0 -x40954_bit0 -x50954_bit0 -x60954_bit0 -x70954_bit0 -x80954_bit0 -x11054_bit0 -x21054_bit0 -x31054_bit0 -x41054_bit0 -x51054_bit0 x61054_bit0 -x71054_bit0 -x81054_bit0 -x91054_bit0 -x10215_bit0 -x10315_bit0 -x20315_bit0 -x10415_bit0 -x20415_bit0 -x30415_bit0 -x10515_bit0 -x20515_bit0 -x30515_bit0 -x40515_bit0 -x10615_bit0 -x20615_bit0 -x30615_bit0 -x40615_bit0 -x50615_bit0 -x10715_bit0 -x20715_bit0 -x30715_bit0 -x40715_bit0 -x50715_bit0 -x60715_bit0 -x10815_bit0 -x20815_bit0 -x30815_bit0 -x40815_bit0 -x50815_bit0 -x60815_bit0 -x70815_bit0 -x10915_bit0 -x20915_bit0 -x30915_bit0 -x40915_bit0 x50915_bit0 -x60915_bit0 -x70915_bit0 -x80915_bit0 -x11015_bit0 -x21015_bit0 -x31015_bit0 -x41015_bit0 -x51015_bit0 -x61015_bit0 -x71015_bit0 -x81015_bit0 -x91015_bit0 -x10225_bit0 -x10325_bit0 -x20325_bit0 -x10425_bit0 -x20425_bit0 -x30425_bit0 -x10525_bit0 -x20525_bit0 -x30525_bit0 -x40525_bit0 -x10625_bit0 -x20625_bit0 -x30625_bit0 -x40625_bit0 -x50625_bit0 -x10725_bit0 -x20725_bit0 -x30725_bit0 -x40725_bit0 -x50725_bit0 -x60725_bit0 -x10825_bit0 -x20825_bit0 x30825_bit0 -x40825_bit0 -x50825_bit0 -x60825_bit0 -x70825_bit0 -x10925_bit0 -x20925_bit0 -x30925_bit0 -x40925_bit0 -x50925_bit0 -x60925_bit0 -x70925_bit0 -x80925_bit0 -x11025_bit0 -x21025_bit0 -x31025_bit0 -x41025_bit0 -x51025_bit0 -x61025_bit0 -x71025_bit0 -x81025_bit0 -x91025_bit0 -x10235_bit0 -x10335_bit0 -x20335_bit0 -x10435_bit0 -x20435_bit0 -x30435_bit0 -x10535_bit0 -x20535_bit0 -x30535_bit0 -x40535_bit0 -x10635_bit0 -x20635_bit0 -x30635_bit0 -x40635_bit0 -x50635_bit0 -x10735_bit0 -x20735_bit0 -x30735_bit0 -x40735_bit0 -x50735_bit0 -x60735_bit0 -x10835_bit0 -x20835_bit0 -x30835_bit0 -x40835_bit0 -x50835_bit0 -x60835_bit0 -x70835_bit0 -x10935_bit0 -x20935_bit0 -x30935_bit0 -x40935_bit0 -x50935_bit0 -x60935_bit0 -x70935_bit0 -x80935_bit0 x11035_bit0 -x21035_bit0 -x31035_bit0 -x41035_bit0 -x51035_bit0 -x61035_bit0 -x71035_bit0 -x81035_bit0 -x91035_bit0 -x10245_bit0 -x10345_bit0 -x20345_bit0 -x10445_bit0 -x20445_bit0 -x30445_bit0 -x10545_bit0 -x20545_bit0 -x30545_bit0 -x40545_bit0 -x10645_bit0 x20645_bit0 -x30645_bit0 -x40645_bit0 -x50645_bit0 -x10745_bit0 -x20745_bit0 -x30745_bit0 -x40745_bit0 -x50745_bit0 -x60745_bit0 -x10845_bit0 -x20845_bit0 -x30845_bit0 -x40845_bit0 -x50845_bit0 -x60845_bit0 -x70845_bit0 -x10945_bit0 -x20945_bit0 -x30945_bit0 -x40945_bit0 -x50945_bit0 -x60945_bit0 -x70945_bit0 -x80945_bit0 -x11045_bit0 -x21045_bit0 -x31045_bit0 -x41045_bit0 -x51045_bit0 -x61045_bit0 -x71045_bit0 -x81045_bit0 -x91045_bit0 -x10255_bit0 -x10355_bit0 -x20355_bit0 -x10455_bit0 -x20455_bit0 -x30455_bit0 -x10555_bit0 -x20555_bit0 -x30555_bit0 -x40555_bit0 -x10655_bit0 -x20655_bit0 -x30655_bit0 -x40655_bit0 -x50655_bit0 -x10755_bit0 -x20755_bit0 -x30755_bit0 x40755_bit0 -x50755_bit0 -x60755_bit0 -x10855_bit0 -x20855_bit0 -x30855_bit0 -x40855_bit0 -x50855_bit0 -x60855_bit0 -x70855_bit0 -x10955_bit0 -x20955_bit0 -x30955_bit0 -x40955_bit0 -x50955_bit0 -x60955_bit0 -x70955_bit0 -x80955_bit0 -x11055_bit0 -x21055_bit0 -x31055_bit0 -x41055_bit0 -x51055_bit0 -x61055_bit0 -x71055_bit0 -x81055_bit0 -x91055_bit0 -x10216_bit0 -x10316_bit0 -x20316_bit0 -x10416_bit0 -x20416_bit0 -x30416_bit0 -x10516_bit0 -x20516_bit0 -x30516_bit0 -x40516_bit0 -x10616_bit0 -x20616_bit0 -x30616_bit0 x40616_bit0 -x50616_bit0 -x10716_bit0 -x20716_bit0 -x30716_bit0 -x40716_bit0 -x50716_bit0 -x60716_bit0 -x10816_bit0 -x20816_bit0 -x30816_bit0 -x40816_bit0 -x50816_bit0 -x60816_bit0 -x70816_bit0 -x10916_bit0 -x20916_bit0 -x30916_bit0 -x40916_bit0 -x50916_bit0 -x60916_bit0 -x70916_bit0 -x80916_bit0 -x11016_bit0 -x21016_bit0 -x31016_bit0 -x41016_bit0 -x51016_bit0 -x61016_bit0 -x71016_bit0 -x81016_bit0 -x91016_bit0 -x10226_bit0 -x10326_bit0 -x20326_bit0 -x10426_bit0 -x20426_bit0 -x30426_bit0 -x10526_bit0 -x20526_bit0 -x30526_bit0 -x40526_bit0 -x10626_bit0 -x20626_bit0 -x30626_bit0 -x40626_bit0 -x50626_bit0 -x10726_bit0 -x20726_bit0 -x30726_bit0 -x40726_bit0 -x50726_bit0 -x60726_bit0 -x10826_bit0 -x20826_bit0 -x30826_bit0 -x40826_bit0 -x50826_bit0 -x60826_bit0 -x70826_bit0 -x10926_bit0 -x20926_bit0 -x30926_bit0 -x40926_bit0 -x50926_bit0 -x60926_bit0 -x70926_bit0 -x80926_bit0 -x11026_bit0 x21026_bit0 -x31026_bit0 -x41026_bit0 -x51026_bit0 -x61026_bit0 -x71026_bit0 -x81026_bit0 -x91026_bit0 -x10236_bit0 -x10336_bit0 -x20336_bit0 -x10436_bit0 -x20436_bit0 -x30436_bit0 -x10536_bit0 -x20536_bit0 -x30536_bit0 -x40536_bit0 -x10636_bit0 -x20636_bit0 -x30636_bit0 -x40636_bit0 -x50636_bit0 -x10736_bit0 -x20736_bit0 -x30736_bit0 -x40736_bit0 -x50736_bit0 -x60736_bit0 x10836_bit0 -x20836_bit0 -x30836_bit0 -x40836_bit0 -x50836_bit0 -x60836_bit0 -x70836_bit0 -x10936_bit0 -x20936_bit0 -x30936_bit0 -x40936_bit0 -x50936_bit0 -x60936_bit0 -x70936_bit0 -x80936_bit0 -x11036_bit0 -x21036_bit0 -x31036_bit0 -x41036_bit0 -x51036_bit0 -x61036_bit0 -x71036_bit0 -x81036_bit0 -x91036_bit0 -x10246_bit0 -x10346_bit0 -x20346_bit0 -x10446_bit0 -x20446_bit0 -x30446_bit0 -x10546_bit0 -x20546_bit0 -x30546_bit0 -x40546_bit0 -x10646_bit0 -x20646_bit0 -x30646_bit0 -x40646_bit0 -x50646_bit0 -x10746_bit0 -x20746_bit0 -x30746_bit0 -x40746_bit0 -x50746_bit0 -x60746_bit0 -x10846_bit0 -x20846_bit0 -x30846_bit0 -x40846_bit0 -x50846_bit0 -x60846_bit0 -x70846_bit0 -x10946_bit0 -x20946_bit0 -x30946_bit0 -x40946_bit0 -x50946_bit0 -x60946_bit0 x70946_bit0 -x80946_bit0 -x11046_bit0 -x21046_bit0 -x31046_bit0 -x41046_bit0 -x51046_bit0 -x61046_bit0 -x71046_bit0 -x81046_bit0 -x91046_bit0 -x10256_bit0 -x10356_bit0 -x20356_bit0 -x10456_bit0 -x20456_bit0 -x30456_bit0 -x10556_bit0 -x20556_bit0 x30556_bit0 -x40556_bit0 -x10656_bit0 -x20656_bit0 -x30656_bit0 -x40656_bit0 -x50656_bit0 -x10756_bit0 -x20756_bit0 -x30756_bit0 -x40756_bit0 -x50756_bit0 -x60756_bit0 -x10856_bit0 -x20856_bit0 -x30856_bit0 -x40856_bit0 -x50856_bit0 -x60856_bit0 -x70856_bit0 -x10956_bit0 -x20956_bit0 -x30956_bit0 -x40956_bit0 -x50956_bit0 -x60956_bit0 -x70956_bit0 -x80956_bit0 -x11056_bit0 -x21056_bit0 -x31056_bit0 -x41056_bit0 -x51056_bit0 -x61056_bit0 -x71056_bit0 -x81056_bit0 -x91056_bit0 -x10217_bit0 -x10317_bit0 -x20317_bit0 -x10417_bit0 -x20417_bit0 -x30417_bit0 -x10517_bit0 -x20517_bit0 -x30517_bit0 -x40517_bit0 -x10617_bit0 -x20617_bit0 -x30617_bit0 -x40617_bit0 -x50617_bit0 -x10717_bit0 -x20717_bit0 -x30717_bit0 -x40717_bit0 -x50717_bit0 -x60717_bit0 -x10817_bit0 -x20817_bit0 -x30817_bit0 -x40817_bit0 -x50817_bit0 -x60817_bit0 -x70817_bit0 -x10917_bit0 -x20917_bit0 -x30917_bit0 -x40917_bit0 -x50917_bit0 -x60917_bit0 -x70917_bit0 -x80917_bit0 -x11017_bit0 -x21017_bit0 -x31017_bit0 -x41017_bit0 -x51017_bit0 -x61017_bit0 -x71017_bit0 x81017_bit0 -x91017_bit0 -x10227_bit0 -x10327_bit0 -x20327_bit0 -x10427_bit0 -x20427_bit0 -x30427_bit0 -x10527_bit0 -x20527_bit0 -x30527_bit0 -x40527_bit0 -x10627_bit0 -x20627_bit0 -x30627_bit0 -x40627_bit0 -x50627_bit0 -x10727_bit0 -x20727_bit0 -x30727_bit0 -x40727_bit0 -x50727_bit0 x60727_bit0 -x10827_bit0 -x20827_bit0 -x30827_bit0 -x40827_bit0 -x50827_bit0 -x60827_bit0 -x70827_bit0 -x10927_bit0 -x20927_bit0 -x30927_bit0 -x40927_bit0 -x50927_bit0 -x60927_bit0 -x70927_bit0 -x80927_bit0 -x11027_bit0 -x21027_bit0 -x31027_bit0 -x41027_bit0 -x51027_bit0 -x61027_bit0 -x71027_bit0 -x81027_bit0 -x91027_bit0 -x10237_bit0 -x10337_bit0 -x20337_bit0 -x10437_bit0 -x20437_bit0 -x30437_bit0 -x10537_bit0 -x20537_bit0 -x30537_bit0 -x40537_bit0 -x10637_bit0 -x20637_bit0 -x30637_bit0 -x40637_bit0 -x50637_bit0 -x10737_bit0 -x20737_bit0 -x30737_bit0 -x40737_bit0 -x50737_bit0 -x60737_bit0 -x10837_bit0 -x20837_bit0 -x30837_bit0 -x40837_bit0 -x50837_bit0 -x60837_bit0 -x70837_bit0 -x10937_bit0 -x20937_bit0 x30937_bit0 -x40937_bit0 -x50937_bit0 -x60937_bit0 -x70937_bit0 -x80937_bit0 -x11037_bit0 -x21037_bit0 -x31037_bit0 -x41037_bit0 -x51037_bit0 -x61037_bit0 -x71037_bit0 -x81037_bit0 -x91037_bit0 -x10247_bit0 -x10347_bit0 -x20347_bit0 x10447_bit0 -x20447_bit0 -x30447_bit0 -x10547_bit0 -x20547_bit0 -x30547_bit0 -x40547_bit0 -x10647_bit0 -x20647_bit0 -x30647_bit0 -x40647_bit0 -x50647_bit0 -x10747_bit0 -x20747_bit0 -x30747_bit0 -x40747_bit0 -x50747_bit0 -x60747_bit0 -x10847_bit0 -x20847_bit0 -x30847_bit0 -x40847_bit0 -x50847_bit0 -x60847_bit0 -x70847_bit0 -x10947_bit0 -x20947_bit0 -x30947_bit0 -x40947_bit0 -x50947_bit0 -x60947_bit0 -x70947_bit0 -x80947_bit0 -x11047_bit0 -x21047_bit0 -x31047_bit0 -x41047_bit0 -x51047_bit0 -x61047_bit0 -x71047_bit0 -x81047_bit0 -x91047_bit0 -x10257_bit0 -x10357_bit0 -x20357_bit0 -x10457_bit0 -x20457_bit0 -x30457_bit0 -x10557_bit0 x20557_bit0 -x30557_bit0 -x40557_bit0 -x10657_bit0 -x20657_bit0 -x30657_bit0 -x40657_bit0 -x50657_bit0 -x10757_bit0 -x20757_bit0 -x30757_bit0 -x40757_bit0 -x50757_bit0 -x60757_bit0 -x10857_bit0 -x20857_bit0 -x30857_bit0 -x40857_bit0 -x50857_bit0 -x60857_bit0 -x70857_bit0 -x10957_bit0 -x20957_bit0 -x30957_bit0 -x40957_bit0 -x50957_bit0 -x60957_bit0 -x70957_bit0 -x80957_bit0 -x11057_bit0 -x21057_bit0 -x31057_bit0 -x41057_bit0 -x51057_bit0 -x61057_bit0 -x71057_bit0 -x81057_bit0 -x91057_bit0 -x10218_bit0 -x10318_bit0 -x20318_bit0 -x10418_bit0 -x20418_bit0 -x30418_bit0 -x10518_bit0 -x20518_bit0 -x30518_bit0 -x40518_bit0 -x10618_bit0 -x20618_bit0 -x30618_bit0 -x40618_bit0 -x50618_bit0 -x10718_bit0 -x20718_bit0 -x30718_bit0 -x40718_bit0 x50718_bit0 -x60718_bit0 -x10818_bit0 -x20818_bit0 -x30818_bit0 -x40818_bit0 -x50818_bit0 -x60818_bit0 -x70818_bit0 -x10918_bit0 -x20918_bit0 -x30918_bit0 -x40918_bit0 -x50918_bit0 -x60918_bit0 -x70918_bit0 -x80918_bit0 -x11018_bit0 -x21018_bit0 -x31018_bit0 -x41018_bit0 -x51018_bit0 -x61018_bit0 -x71018_bit0 -x81018_bit0 -x91018_bit0 -x10228_bit0 -x10328_bit0 -x20328_bit0 -x10428_bit0 x20428_bit0 -x30428_bit0 -x10528_bit0 -x20528_bit0 -x30528_bit0 -x40528_bit0 -x10628_bit0 -x20628_bit0 -x30628_bit0 -x40628_bit0 -x50628_bit0 -x10728_bit0 -x20728_bit0 -x30728_bit0 -x40728_bit0 -x50728_bit0 -x60728_bit0 -x10828_bit0 -x20828_bit0 -x30828_bit0 -x40828_bit0 -x50828_bit0 -x60828_bit0 -x70828_bit0 -x10928_bit0 -x20928_bit0 -x30928_bit0 -x40928_bit0 -x50928_bit0 -x60928_bit0 -x70928_bit0 -x80928_bit0 -x11028_bit0 -x21028_bit0 -x31028_bit0 -x41028_bit0 -x51028_bit0 -x61028_bit0 -x71028_bit0 -x81028_bit0 -x91028_bit0 -x10238_bit0 -x10338_bit0 -x20338_bit0 -x10438_bit0 -x20438_bit0 -x30438_bit0 -x10538_bit0 -x20538_bit0 -x30538_bit0 -x40538_bit0 -x10638_bit0 -x20638_bit0 -x30638_bit0 -x40638_bit0 -x50638_bit0 -x10738_bit0 -x20738_bit0 -x30738_bit0 -x40738_bit0 -x50738_bit0 -x60738_bit0 -x10838_bit0 -x20838_bit0 -x30838_bit0 -x40838_bit0 -x50838_bit0 x60838_bit0 -x70838_bit0 -x10938_bit0 -x20938_bit0 -x30938_bit0 -x40938_bit0 -x50938_bit0 -x60938_bit0 -x70938_bit0 -x80938_bit0 -x11038_bit0 -x21038_bit0 -x31038_bit0 -x41038_bit0 -x51038_bit0 -x61038_bit0 -x71038_bit0 -x81038_bit0 -x91038_bit0 -x10248_bit0 -x10348_bit0 -x20348_bit0 -x10448_bit0 -x20448_bit0 -x30448_bit0 -x10548_bit0 -x20548_bit0 -x30548_bit0 -x40548_bit0 -x10648_bit0 -x20648_bit0 -x30648_bit0 -x40648_bit0 -x50648_bit0 -x10748_bit0 -x20748_bit0 -x30748_bit0 -x40748_bit0 -x50748_bit0 -x60748_bit0 -x10848_bit0 -x20848_bit0 -x30848_bit0 -x40848_bit0 -x50848_bit0 -x60848_bit0 -x70848_bit0 -x10948_bit0 -x20948_bit0 -x30948_bit0 -x40948_bit0 -x50948_bit0 -x60948_bit0 -x70948_bit0 -x80948_bit0 -x11048_bit0 -x21048_bit0 x31048_bit0 -x41048_bit0 -x51048_bit0 -x61048_bit0 -x71048_bit0 -x81048_bit0 -x91048_bit0 -x10258_bit0 -x10358_bit0 -x20358_bit0 -x10458_bit0 -x20458_bit0 -x30458_bit0 -x10558_bit0 -x20558_bit0 -x30558_bit0 -x40558_bit0 -x10658_bit0 -x20658_bit0 -x30658_bit0 -x40658_bit0 -x50658_bit0 -x10758_bit0 -x20758_bit0 -x30758_bit0 -x40758_bit0 -x50758_bit0 -x60758_bit0 -x10858_bit0 -x20858_bit0 -x30858_bit0 -x40858_bit0 -x50858_bit0 -x60858_bit0 -x70858_bit0 x10958_bit0 -x20958_bit0 -x30958_bit0 -x40958_bit0 -x50958_bit0 -x60958_bit0 -x70958_bit0 -x80958_bit0 -x11058_bit0 -x21058_bit0 -x31058_bit0 -x41058_bit0 -x51058_bit0 -x61058_bit0 -x71058_bit0 -x81058_bit0 -x91058_bit0
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/13930/stat): 13930 (minisat+_script) R 13929 13930 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1733005213 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/13930/statm): 174 3 169 147 0 27 0 [pid=13930] 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=13931 New process pid=13932 New process pid=13933 execve syscall for /bin/sed executable One traced child (pid=13932) 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=13933) exited with status: 0 One traced child (pid=13931) exited with status: 0 New process pid=13934 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-10teams.opb [startup+10.0031 s] Raw data (loadavg): 0.99 0.98 0.99 1/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) T 13930 13930 20602 0 -1 0 2541 0 0 0 970 11 0 0 25 0 1 0 1733005218 11149312 2479 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13934/statm): 2722 2479 145 145 0 2577 0 [pid=13934] vsize: 10888 Current children cumulated CPU time (s) 9.81 Current children cumulated vsize (Kb) 13012 [startup+20.0038 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 9098 0 0 0 1932 32 0 0 25 0 1 0 1733005218 34197504 7715 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 8349 7715 145 145 0 8204 0 [pid=13934] vsize: 33396 Current children cumulated CPU time (s) 19.64 Current children cumulated vsize (Kb) 35520 [startup+30.0055 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 9483 0 0 0 2925 34 0 0 25 0 1 0 1733005218 35799040 8100 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 8740 8100 145 145 0 8595 0 [pid=13934] vsize: 34960 Current children cumulated CPU time (s) 29.59 Current children cumulated vsize (Kb) 37084 [startup+40.0062 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 9957 0 0 0 3918 37 0 0 25 0 1 0 1733005218 37732352 8574 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 9212 8574 145 145 0 9067 0 [pid=13934] vsize: 36848 Current children cumulated CPU time (s) 39.55 Current children cumulated vsize (Kb) 38972 [startup+50.0079 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 10465 0 0 0 4910 41 0 0 25 0 1 0 1733005218 39804928 9082 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 9718 9082 145 145 0 9573 0 [pid=13934] vsize: 38872 Current children cumulated CPU time (s) 49.51 Current children cumulated vsize (Kb) 40996 [startup+60.0085 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 10867 0 0 0 5905 42 0 0 25 0 1 0 1733005218 41447424 9484 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 10119 9484 145 145 0 9974 0 [pid=13934] vsize: 40476 Current children cumulated CPU time (s) 59.47 Current children cumulated vsize (Kb) 42600 [startup+70.0092 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 11319 0 0 0 6900 45 0 0 25 0 1 0 1733005218 42889216 9850 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 10471 9850 145 145 0 10326 0 [pid=13934] vsize: 41884 Current children cumulated CPU time (s) 69.45 Current children cumulated vsize (Kb) 44008 [startup+80.0099 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 11675 0 0 0 7894 47 0 0 25 0 1 0 1733005218 44396544 10206 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 10839 10206 145 145 0 10694 0 [pid=13934] vsize: 43356 Current children cumulated CPU time (s) 79.41 Current children cumulated vsize (Kb) 45480 [startup+90.0106 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 12142 0 0 0 8886 51 0 0 25 0 1 0 1733005218 46305280 10673 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 11305 10673 145 145 0 11160 0 [pid=13934] vsize: 45220 Current children cumulated CPU time (s) 89.37 Current children cumulated vsize (Kb) 47344 [startup+100.01 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 12552 0 0 0 9879 53 0 0 25 0 1 0 1733005218 47976448 11083 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 11713 11083 145 145 0 11568 0 [pid=13934] vsize: 46852 Current children cumulated CPU time (s) 99.32 Current children cumulated vsize (Kb) 48976 [startup+110.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 12938 0 0 0 10874 57 0 0 25 0 1 0 1733005218 49553408 11469 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 12098 11469 145 145 0 11953 0 [pid=13934] vsize: 48392 Current children cumulated CPU time (s) 109.31 Current children cumulated vsize (Kb) 50516 [startup+120.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 13387 0 0 0 11866 61 0 0 25 0 1 0 1733005218 51384320 11918 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 12545 11918 145 145 0 12400 0 [pid=13934] vsize: 50180 Current children cumulated CPU time (s) 119.27 Current children cumulated vsize (Kb) 52304 [startup+130.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 13870 0 0 0 12858 64 0 0 25 0 1 0 1733005218 53358592 12401 4294967295 134512640 135094434 3221224432 3221223024 134556921 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 13027 12401 145 145 0 12882 0 [pid=13934] vsize: 52108 Current children cumulated CPU time (s) 129.22 Current children cumulated vsize (Kb) 54232 [startup+140.013 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 14278 0 0 0 13852 67 0 0 25 0 1 0 1733005218 55021568 12809 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 13433 12809 145 145 0 13288 0 [pid=13934] vsize: 53732 Current children cumulated CPU time (s) 139.19 Current children cumulated vsize (Kb) 55856 [startup+150.014 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 14679 0 0 0 14845 70 0 0 25 0 1 0 1733005218 56659968 13210 4294967295 134512640 135094434 3221224432 3221223056 134557683 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 13833 13210 145 145 0 13688 0 [pid=13934] vsize: 55332 Current children cumulated CPU time (s) 149.15 Current children cumulated vsize (Kb) 57456 [startup+160.014 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 15104 0 0 0 15838 73 0 0 25 0 1 0 1733005218 58392576 13635 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 14256 13635 145 145 0 14111 0 [pid=13934] vsize: 57024 Current children cumulated CPU time (s) 159.11 Current children cumulated vsize (Kb) 59148 [startup+170.014 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 15514 0 0 0 16832 76 0 0 25 0 1 0 1733005218 60067840 14045 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 14665 14045 145 145 0 14520 0 [pid=13934] vsize: 58660 Current children cumulated CPU time (s) 169.08 Current children cumulated vsize (Kb) 60784 [startup+180.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 15917 0 0 0 17824 79 0 0 25 0 1 0 1733005218 61714432 14448 4294967295 134512640 135094434 3221224432 3221223104 134555680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 15067 14448 145 145 0 14922 0 [pid=13934] vsize: 60268 Current children cumulated CPU time (s) 179.03 Current children cumulated vsize (Kb) 62392 [startup+190.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 16353 0 0 0 18817 82 0 0 25 0 1 0 1733005218 63623168 14884 4294967295 134512640 135094434 3221224432 3221223080 134558037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 15533 14884 145 145 0 15388 0 [pid=13934] vsize: 62132 Current children cumulated CPU time (s) 188.99 Current children cumulated vsize (Kb) 64256 [startup+200.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 16766 0 0 0 19811 85 0 0 25 0 1 0 1733005218 65310720 15297 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 15945 15297 145 145 0 15800 0 [pid=13934] vsize: 63780 Current children cumulated CPU time (s) 198.96 Current children cumulated vsize (Kb) 65904 [startup+210.016 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 17170 0 0 0 20806 87 0 0 25 0 1 0 1733005218 66957312 15701 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 16347 15701 145 145 0 16202 0 [pid=13934] vsize: 65388 Current children cumulated CPU time (s) 208.93 Current children cumulated vsize (Kb) 67512 [startup+220.016 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 17540 0 0 0 21799 90 0 0 25 0 1 0 1733005218 68468736 16071 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 16716 16071 145 145 0 16571 0 [pid=13934] vsize: 66864 Current children cumulated CPU time (s) 218.89 Current children cumulated vsize (Kb) 68988 [startup+230.017 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 17882 0 0 0 22793 93 0 0 25 0 1 0 1733005218 69865472 16413 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 17057 16413 145 145 0 16912 0 [pid=13934] vsize: 68228 Current children cumulated CPU time (s) 228.86 Current children cumulated vsize (Kb) 70352 [startup+240.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 18221 0 0 0 23789 95 0 0 25 0 1 0 1733005218 71249920 16752 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 17395 16752 145 145 0 17250 0 [pid=13934] vsize: 69580 Current children cumulated CPU time (s) 238.84 Current children cumulated vsize (Kb) 71704 [startup+250.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 18568 0 0 0 24783 98 0 0 25 0 1 0 1733005218 72667136 17099 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 17741 17099 145 145 0 17596 0 [pid=13934] vsize: 70964 Current children cumulated CPU time (s) 248.81 Current children cumulated vsize (Kb) 73088 [startup+260.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 18979 0 0 0 25776 100 0 0 25 0 1 0 1733005218 74346496 17510 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 18151 17510 145 145 0 18006 0 [pid=13934] vsize: 72604 Current children cumulated CPU time (s) 258.76 Current children cumulated vsize (Kb) 74728 [startup+270.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 19367 0 0 0 26771 103 0 0 25 0 1 0 1733005218 75927552 17898 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 18537 17898 145 145 0 18392 0 [pid=13934] vsize: 74148 Current children cumulated CPU time (s) 268.74 Current children cumulated vsize (Kb) 76272 [startup+280.019 s] Raw data (loadavg): 1.07 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 19741 0 0 0 27766 104 0 0 25 0 1 0 1733005218 77455360 18272 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 18910 18272 145 145 0 18765 0 [pid=13934] vsize: 75640 Current children cumulated CPU time (s) 278.7 Current children cumulated vsize (Kb) 77764 [startup+290.019 s] Raw data (loadavg): 1.14 1.02 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 20139 0 0 0 28758 108 0 0 25 0 1 0 1733005218 79081472 18670 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 19307 18670 145 145 0 19162 0 [pid=13934] vsize: 77228 Current children cumulated CPU time (s) 288.66 Current children cumulated vsize (Kb) 79352 [startup+300.019 s] Raw data (loadavg): 1.11 1.02 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 20568 0 0 0 29752 111 0 0 25 0 1 0 1733005218 80830464 19099 4294967295 134512640 135094434 3221224432 3221223024 134556914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 19734 19099 145 145 0 19589 0 [pid=13934] vsize: 78936 Current children cumulated CPU time (s) 298.63 Current children cumulated vsize (Kb) 81060 [startup+310.02 s] Raw data (loadavg): 1.10 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 21002 0 0 0 30745 114 0 0 25 0 1 0 1733005218 82604032 19533 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 20167 19533 145 145 0 20022 0 [pid=13934] vsize: 80668 Current children cumulated CPU time (s) 308.59 Current children cumulated vsize (Kb) 82792 [startup+320.019 s] Raw data (loadavg): 1.08 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 21392 0 0 0 31740 117 0 0 25 0 1 0 1733005218 84197376 19923 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 20556 19923 145 145 0 20411 0 [pid=13934] vsize: 82224 Current children cumulated CPU time (s) 318.57 Current children cumulated vsize (Kb) 84348 [startup+330.02 s] Raw data (loadavg): 1.07 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 21775 0 0 0 32734 120 0 0 25 0 1 0 1733005218 85762048 20306 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 20938 20306 145 145 0 20793 0 [pid=13934] vsize: 83752 Current children cumulated CPU time (s) 328.54 Current children cumulated vsize (Kb) 85876 [startup+340.021 s] Raw data (loadavg): 1.06 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 22164 0 0 0 33727 123 0 0 25 0 1 0 1733005218 87351296 20695 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 21326 20695 145 145 0 21181 0 [pid=13934] vsize: 85304 Current children cumulated CPU time (s) 338.5 Current children cumulated vsize (Kb) 87428 [startup+350.02 s] Raw data (loadavg): 1.05 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 22537 0 0 0 34720 126 0 0 25 0 1 0 1733005218 88875008 21068 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 21698 21068 145 145 0 21553 0 [pid=13934] vsize: 86792 Current children cumulated CPU time (s) 348.46 Current children cumulated vsize (Kb) 88916 [startup+360.021 s] Raw data (loadavg): 1.04 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 22882 0 0 0 35713 129 0 0 25 0 1 0 1733005218 90279936 21413 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 22041 21413 145 145 0 21896 0 [pid=13934] vsize: 88164 Current children cumulated CPU time (s) 358.42 Current children cumulated vsize (Kb) 90288 [startup+370.021 s] Raw data (loadavg): 1.03 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 23228 0 0 0 36709 130 0 0 25 0 1 0 1733005218 91693056 21759 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 22386 21759 145 145 0 22241 0 [pid=13934] vsize: 89544 Current children cumulated CPU time (s) 368.39 Current children cumulated vsize (Kb) 91668 [startup+380.021 s] Raw data (loadavg): 1.03 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 23605 0 0 0 37702 134 0 0 25 0 1 0 1733005218 93233152 22136 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 22762 22136 145 145 0 22617 0 [pid=13934] vsize: 91048 Current children cumulated CPU time (s) 378.36 Current children cumulated vsize (Kb) 93172 [startup+390.022 s] Raw data (loadavg): 1.02 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 23976 0 0 0 38696 135 0 0 25 0 1 0 1733005218 94748672 22507 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 23132 22507 145 145 0 22987 0 [pid=13934] vsize: 92528 Current children cumulated CPU time (s) 388.31 Current children cumulated vsize (Kb) 94652 [startup+400.023 s] Raw data (loadavg): 1.02 1.01 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 24370 0 0 0 39689 139 0 0 25 0 1 0 1733005218 96358400 22901 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 23525 22901 145 145 0 23380 0 [pid=13934] vsize: 94100 Current children cumulated CPU time (s) 398.28 Current children cumulated vsize (Kb) 96224 [startup+410.023 s] Raw data (loadavg): 1.02 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 24779 0 0 0 40682 140 0 0 25 0 1 0 1733005218 98029568 23310 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 23933 23310 145 145 0 23788 0 [pid=13934] vsize: 95732 Current children cumulated CPU time (s) 408.22 Current children cumulated vsize (Kb) 97856 [startup+420.024 s] Raw data (loadavg): 1.01 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 25256 0 0 0 41675 144 0 0 25 0 1 0 1733005218 99979264 23787 4294967295 134512640 135094434 3221224432 3221223024 134557316 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 24409 23787 145 145 0 24264 0 [pid=13934] vsize: 97636 Current children cumulated CPU time (s) 418.19 Current children cumulated vsize (Kb) 99760 [startup+430.025 s] Raw data (loadavg): 1.01 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 25680 0 0 0 42669 148 0 0 25 0 1 0 1733005218 101711872 24211 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 24832 24211 145 145 0 24687 0 [pid=13934] vsize: 99328 Current children cumulated CPU time (s) 428.17 Current children cumulated vsize (Kb) 101452 [startup+440.025 s] Raw data (loadavg): 1.01 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 26117 0 0 0 43662 151 0 0 25 0 1 0 1733005218 103497728 24648 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 25268 24648 145 145 0 25123 0 [pid=13934] vsize: 101072 Current children cumulated CPU time (s) 438.13 Current children cumulated vsize (Kb) 103196 [startup+450.026 s] Raw data (loadavg): 1.01 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 26533 0 0 0 44655 154 0 0 25 0 1 0 1733005218 105197568 25064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 25683 25064 145 145 0 25538 0 [pid=13934] vsize: 102732 Current children cumulated CPU time (s) 448.09 Current children cumulated vsize (Kb) 104856 [startup+460.027 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 26955 0 0 0 45646 157 0 0 25 0 1 0 1733005218 107184128 25486 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 26168 25486 145 145 0 26023 0 [pid=13934] vsize: 104672 Current children cumulated CPU time (s) 458.03 Current children cumulated vsize (Kb) 106796 [startup+470.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 27396 0 0 0 46640 160 0 0 25 0 1 0 1733005218 108986368 25927 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 26608 25927 145 145 0 26463 0 [pid=13934] vsize: 106432 Current children cumulated CPU time (s) 468 Current children cumulated vsize (Kb) 108556 [startup+480.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 27819 0 0 0 47634 163 0 0 25 0 1 0 1733005218 110714880 26350 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 27030 26350 145 145 0 26885 0 [pid=13934] vsize: 108120 Current children cumulated CPU time (s) 477.97 Current children cumulated vsize (Kb) 110244 [startup+490.029 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 28254 0 0 0 48628 166 0 0 25 0 1 0 1733005218 112496640 26785 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 27465 26785 145 145 0 27320 0 [pid=13934] vsize: 109860 Current children cumulated CPU time (s) 487.94 Current children cumulated vsize (Kb) 111984 [startup+500.03 s] Raw data (loadavg): 1.00 1.00 1.00 1/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) T 13930 13930 20602 0 -1 0 28660 0 0 0 49623 168 0 0 25 0 1 0 1733005218 114155520 27191 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13934/statm): 27870 27191 145 145 0 27725 0 [pid=13934] vsize: 111480 Current children cumulated CPU time (s) 497.91 Current children cumulated vsize (Kb) 113604 [startup+510.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 29091 0 0 0 50616 170 0 0 25 0 1 0 1733005218 115916800 27622 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 28300 27622 145 145 0 28155 0 [pid=13934] vsize: 113200 Current children cumulated CPU time (s) 507.86 Current children cumulated vsize (Kb) 115324 [startup+520.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 29535 0 0 0 51612 173 0 0 25 0 1 0 1733005218 117735424 28066 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 28744 28066 145 145 0 28599 0 [pid=13934] vsize: 114976 Current children cumulated CPU time (s) 517.85 Current children cumulated vsize (Kb) 117100 [startup+530.031 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 29959 0 0 0 52606 176 0 0 25 0 1 0 1733005218 119468032 28490 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 29167 28490 145 145 0 29022 0 [pid=13934] vsize: 116668 Current children cumulated CPU time (s) 527.82 Current children cumulated vsize (Kb) 118792 [startup+540.031 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 30398 0 0 0 53602 178 0 0 25 0 1 0 1733005218 121266176 28929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 29606 28929 145 145 0 29461 0 [pid=13934] vsize: 118424 Current children cumulated CPU time (s) 537.8 Current children cumulated vsize (Kb) 120548 [startup+550.031 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 30842 0 0 0 54595 180 0 0 25 0 1 0 1733005218 123080704 29373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 30049 29373 145 145 0 29904 0 [pid=13934] vsize: 120196 Current children cumulated CPU time (s) 547.75 Current children cumulated vsize (Kb) 122320 [startup+560.032 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 31161 0 0 0 55591 182 0 0 25 0 1 0 1733005218 124383232 29692 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 30367 29692 145 145 0 30222 0 [pid=13934] vsize: 121468 Current children cumulated CPU time (s) 557.73 Current children cumulated vsize (Kb) 123592 [startup+570.032 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 31506 0 0 0 56585 185 0 0 25 0 1 0 1733005218 125792256 30037 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 30711 30037 145 145 0 30566 0 [pid=13934] vsize: 122844 Current children cumulated CPU time (s) 567.7 Current children cumulated vsize (Kb) 124968 [startup+580.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 31878 0 0 0 57577 188 0 0 25 0 1 0 1733005218 127311872 30409 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 31082 30409 145 145 0 30937 0 [pid=13934] vsize: 124328 Current children cumulated CPU time (s) 577.65 Current children cumulated vsize (Kb) 126452 [startup+590.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 32253 0 0 0 58571 190 0 0 25 0 1 0 1733005218 128843776 30784 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 31456 30784 145 145 0 31311 0 [pid=13934] vsize: 125824 Current children cumulated CPU time (s) 587.61 Current children cumulated vsize (Kb) 127948 [startup+600.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 32599 0 0 0 59565 192 0 0 25 0 1 0 1733005218 130256896 31130 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 31801 31130 145 145 0 31656 0 [pid=13934] vsize: 127204 Current children cumulated CPU time (s) 597.57 Current children cumulated vsize (Kb) 129328 [startup+610.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 32979 0 0 0 60558 195 0 0 25 0 1 0 1733005218 131809280 31510 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 32180 31510 145 145 0 32035 0 [pid=13934] vsize: 128720 Current children cumulated CPU time (s) 607.53 Current children cumulated vsize (Kb) 130844 [startup+620.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 33359 0 0 0 61553 198 0 0 25 0 1 0 1733005218 133365760 31890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 32560 31890 145 145 0 32415 0 [pid=13934] vsize: 130240 Current children cumulated CPU time (s) 617.51 Current children cumulated vsize (Kb) 132364 [startup+630.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 33711 0 0 0 62546 202 0 0 25 0 1 0 1733005218 134811648 32242 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 32913 32242 145 145 0 32768 0 [pid=13934] vsize: 131652 Current children cumulated CPU time (s) 627.48 Current children cumulated vsize (Kb) 133776 [startup+640.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 34060 0 0 0 63542 204 0 0 25 0 1 0 1733005218 136241152 32591 4294967295 134512640 135094434 3221224432 3221223024 134552003 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 33262 32591 145 145 0 33117 0 [pid=13934] vsize: 133048 Current children cumulated CPU time (s) 637.46 Current children cumulated vsize (Kb) 135172 [startup+650.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 34422 0 0 0 64536 207 0 0 25 0 1 0 1733005218 137719808 32953 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 33623 32953 145 145 0 33478 0 [pid=13934] vsize: 134492 Current children cumulated CPU time (s) 647.43 Current children cumulated vsize (Kb) 136616 [startup+660.037 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 34769 0 0 0 65530 209 0 0 25 0 1 0 1733005218 139141120 33300 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 33970 33300 145 145 0 33825 0 [pid=13934] vsize: 135880 Current children cumulated CPU time (s) 657.39 Current children cumulated vsize (Kb) 138004 [startup+670.037 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 35140 0 0 0 66526 211 0 0 25 0 1 0 1733005218 140660736 33671 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 34341 33671 145 145 0 34196 0 [pid=13934] vsize: 137364 Current children cumulated CPU time (s) 667.37 Current children cumulated vsize (Kb) 139488 [startup+680.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 35460 0 0 0 67521 213 0 0 25 0 1 0 1733005218 141967360 33991 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 34660 33991 145 145 0 34515 0 [pid=13934] vsize: 138640 Current children cumulated CPU time (s) 677.34 Current children cumulated vsize (Kb) 140764 [startup+690.039 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 35786 0 0 0 68517 215 0 0 25 0 1 0 1733005218 143298560 34317 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 34985 34317 145 145 0 34840 0 [pid=13934] vsize: 139940 Current children cumulated CPU time (s) 687.32 Current children cumulated vsize (Kb) 142064 [startup+700.039 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 36139 0 0 0 69511 218 0 0 25 0 1 0 1733005218 144752640 34670 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 35340 34670 145 145 0 35195 0 [pid=13934] vsize: 141360 Current children cumulated CPU time (s) 697.29 Current children cumulated vsize (Kb) 143484 [startup+710.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 36481 0 0 0 70506 221 0 0 25 0 1 0 1733005218 146149376 35012 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 35681 35012 145 145 0 35536 0 [pid=13934] vsize: 142724 Current children cumulated CPU time (s) 707.27 Current children cumulated vsize (Kb) 144848 [startup+720.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 36799 0 0 0 71502 222 0 0 25 0 1 0 1733005218 147464192 35330 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 36002 35330 145 145 0 35857 0 [pid=13934] vsize: 144008 Current children cumulated CPU time (s) 717.24 Current children cumulated vsize (Kb) 146132 [startup+730.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 37150 0 0 0 72497 224 0 0 25 0 1 0 1733005218 148897792 35681 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 36352 35681 145 145 0 36207 0 [pid=13934] vsize: 145408 Current children cumulated CPU time (s) 727.21 Current children cumulated vsize (Kb) 147532 [startup+740.041 s] Raw data (loadavg): 1.00 1.00 1.00 1/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) T 13930 13930 20602 0 -1 0 37536 0 0 0 73494 226 0 0 25 0 1 0 1733005218 150478848 36067 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13934/statm): 36738 36067 145 145 0 36593 0 [pid=13934] vsize: 146952 Current children cumulated CPU time (s) 737.2 Current children cumulated vsize (Kb) 149076 [startup+750.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 37897 0 0 0 74489 229 0 0 25 0 1 0 1733005218 151961600 36428 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 37100 36428 145 145 0 36955 0 [pid=13934] vsize: 148400 Current children cumulated CPU time (s) 747.18 Current children cumulated vsize (Kb) 150524 [startup+760.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 38245 0 0 0 75484 231 0 0 25 0 1 0 1733005218 153387008 36776 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 37448 36776 145 145 0 37303 0 [pid=13934] vsize: 149792 Current children cumulated CPU time (s) 757.15 Current children cumulated vsize (Kb) 151916 [startup+770.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 38568 0 0 0 76480 233 0 0 25 0 1 0 1733005218 154705920 37099 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 37770 37099 145 145 0 37625 0 [pid=13934] vsize: 151080 Current children cumulated CPU time (s) 767.13 Current children cumulated vsize (Kb) 153204 [startup+780.044 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 38873 0 0 0 77477 234 0 0 25 0 1 0 1733005218 155967488 37404 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 38078 37404 145 145 0 37933 0 [pid=13934] vsize: 152312 Current children cumulated CPU time (s) 777.11 Current children cumulated vsize (Kb) 154436 [startup+790.044 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 39201 0 0 0 78473 236 0 0 25 0 1 0 1733005218 157310976 37732 4294967295 134512640 135094434 3221224432 3221223104 134556336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 38406 37732 145 145 0 38261 0 [pid=13934] vsize: 153624 Current children cumulated CPU time (s) 787.09 Current children cumulated vsize (Kb) 155748 [startup+800.045 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 39483 0 0 0 79469 238 0 0 25 0 1 0 1733005218 158474240 38014 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 38690 38014 145 145 0 38545 0 [pid=13934] vsize: 154760 Current children cumulated CPU time (s) 797.07 Current children cumulated vsize (Kb) 156884 [startup+810.046 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 39818 0 0 0 80465 240 0 0 25 0 1 0 1733005218 159846400 38349 4294967295 134512640 135094434 3221224432 3221223024 134557055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 39025 38349 145 145 0 38880 0 [pid=13934] vsize: 156100 Current children cumulated CPU time (s) 807.05 Current children cumulated vsize (Kb) 158224 [startup+820.045 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 40168 0 0 0 81460 242 0 0 25 0 1 0 1733005218 161288192 38699 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 39377 38699 145 145 0 39232 0 [pid=13934] vsize: 157508 Current children cumulated CPU time (s) 817.02 Current children cumulated vsize (Kb) 159632 [startup+830.046 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 40522 0 0 0 82455 244 0 0 25 0 1 0 1733005218 162738176 39053 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 39731 39053 145 145 0 39586 0 [pid=13934] vsize: 158924 Current children cumulated CPU time (s) 826.99 Current children cumulated vsize (Kb) 161048 [startup+840.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 40894 0 0 0 83451 246 0 0 25 0 1 0 1733005218 164261888 39425 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 40103 39425 145 145 0 39958 0 [pid=13934] vsize: 160412 Current children cumulated CPU time (s) 836.97 Current children cumulated vsize (Kb) 162536 [startup+850.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 41243 0 0 0 84446 248 0 0 25 0 1 0 1733005218 165695488 39774 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 40453 39774 145 145 0 40308 0 [pid=13934] vsize: 161812 Current children cumulated CPU time (s) 846.94 Current children cumulated vsize (Kb) 163936 [startup+860.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 41575 0 0 0 85440 250 0 0 25 0 1 0 1733005218 167047168 40106 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 40783 40106 145 145 0 40638 0 [pid=13934] vsize: 163132 Current children cumulated CPU time (s) 856.9 Current children cumulated vsize (Kb) 165256 [startup+870.048 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 41855 0 0 0 86436 252 0 0 25 0 1 0 1733005218 168189952 40386 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 41062 40386 145 145 0 40917 0 [pid=13934] vsize: 164248 Current children cumulated CPU time (s) 866.88 Current children cumulated vsize (Kb) 166372 [startup+880.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 42121 0 0 0 87431 254 0 0 25 0 1 0 1733005218 169275392 40652 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 41327 40652 145 145 0 41182 0 [pid=13934] vsize: 165308 Current children cumulated CPU time (s) 876.85 Current children cumulated vsize (Kb) 167432 [startup+890.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 42426 0 0 0 88426 257 0 0 25 0 1 0 1733005218 170520576 40957 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 41631 40957 145 145 0 41486 0 [pid=13934] vsize: 166524 Current children cumulated CPU time (s) 886.83 Current children cumulated vsize (Kb) 168648 [startup+900.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 42725 0 0 0 89420 259 0 0 25 0 1 0 1733005218 171741184 41256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 41929 41256 145 145 0 41784 0 [pid=13934] vsize: 167716 Current children cumulated CPU time (s) 896.79 Current children cumulated vsize (Kb) 169840 [startup+910.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 43005 0 0 0 90414 261 0 0 25 0 1 0 1733005218 172883968 41536 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 42208 41536 145 145 0 42063 0 [pid=13934] vsize: 168832 Current children cumulated CPU time (s) 906.75 Current children cumulated vsize (Kb) 170956 [startup+920.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 43350 0 0 0 91408 264 0 0 25 0 1 0 1733005218 174288896 41881 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 42551 41881 145 145 0 42406 0 [pid=13934] vsize: 170204 Current children cumulated CPU time (s) 916.72 Current children cumulated vsize (Kb) 172328 [startup+930.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 43662 0 0 0 92403 266 0 0 25 0 1 0 1733005218 175562752 42193 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 42862 42193 145 145 0 42717 0 [pid=13934] vsize: 171448 Current children cumulated CPU time (s) 926.69 Current children cumulated vsize (Kb) 173572 [startup+940.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 43968 0 0 0 93399 268 0 0 25 0 1 0 1733005218 176812032 42499 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 43167 42499 145 145 0 43022 0 [pid=13934] vsize: 172668 Current children cumulated CPU time (s) 936.67 Current children cumulated vsize (Kb) 174792 [startup+950.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 44287 0 0 0 94395 270 0 0 25 0 1 0 1733005218 178114560 42818 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 43485 42818 145 145 0 43340 0 [pid=13934] vsize: 173940 Current children cumulated CPU time (s) 946.65 Current children cumulated vsize (Kb) 176064 [startup+960.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 44597 0 0 0 95389 272 0 0 25 0 1 0 1733005218 179380224 43128 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 43794 43128 145 145 0 43649 0 [pid=13934] vsize: 175176 Current children cumulated CPU time (s) 956.61 Current children cumulated vsize (Kb) 177300 [startup+970.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 44962 0 0 0 96385 274 0 0 25 0 1 0 1733005218 180871168 43493 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 44158 43493 145 145 0 44013 0 [pid=13934] vsize: 176632 Current children cumulated CPU time (s) 966.59 Current children cumulated vsize (Kb) 178756 [startup+980.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 45374 0 0 0 97379 277 0 0 25 0 1 0 1733005218 182558720 43905 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 44570 43905 145 145 0 44425 0 [pid=13934] vsize: 178280 Current children cumulated CPU time (s) 976.56 Current children cumulated vsize (Kb) 180404 [startup+990.054 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 45742 0 0 0 98374 279 0 0 25 0 1 0 1733005218 184061952 44273 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 44937 44273 145 145 0 44792 0 [pid=13934] vsize: 179748 Current children cumulated CPU time (s) 986.53 Current children cumulated vsize (Kb) 181872 [startup+1000.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 46069 0 0 0 99368 282 0 0 25 0 1 0 1733005218 185397248 44600 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 45263 44600 145 145 0 45118 0 [pid=13934] vsize: 181052 Current children cumulated CPU time (s) 996.5 Current children cumulated vsize (Kb) 183176 [startup+1010.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 46395 0 0 0 100363 285 0 0 25 0 1 0 1733005218 186728448 44926 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13934/statm): 45588 44926 145 145 0 45443 0 [pid=13934] vsize: 182352 Current children cumulated CPU time (s) 1006.48 Current children cumulated vsize (Kb) 184476 [startup+1020.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 46700 0 0 0 101359 287 0 0 25 0 1 0 1733005218 187973632 45231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 45892 45231 145 145 0 45747 0 [pid=13934] vsize: 183568 Current children cumulated CPU time (s) 1016.46 Current children cumulated vsize (Kb) 185692 [startup+1030.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 47007 0 0 0 102353 289 0 0 25 0 1 0 1733005218 189227008 45538 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 46198 45538 145 145 0 46053 0 [pid=13934] vsize: 184792 Current children cumulated CPU time (s) 1026.42 Current children cumulated vsize (Kb) 186916 [startup+1040.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 47288 0 0 0 103348 291 0 0 25 0 1 0 1733005218 190382080 45819 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 46480 45819 145 145 0 46335 0 [pid=13934] vsize: 185920 Current children cumulated CPU time (s) 1036.39 Current children cumulated vsize (Kb) 188044 [startup+1050.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 47566 0 0 0 104343 293 0 0 25 0 1 0 1733005218 191516672 46097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 46757 46097 145 145 0 46612 0 [pid=13934] vsize: 187028 Current children cumulated CPU time (s) 1046.36 Current children cumulated vsize (Kb) 189152 [startup+1060.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 47874 0 0 0 105337 296 0 0 25 0 1 0 1733005218 192778240 46405 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 47065 46405 145 145 0 46920 0 [pid=13934] vsize: 188260 Current children cumulated CPU time (s) 1056.33 Current children cumulated vsize (Kb) 190384 [startup+1070.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 48153 0 0 0 106332 298 0 0 25 0 1 0 1733005218 193916928 46684 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 47343 46684 145 145 0 47198 0 [pid=13934] vsize: 189372 Current children cumulated CPU time (s) 1066.3 Current children cumulated vsize (Kb) 191496 [startup+1080.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 48464 0 0 0 107328 300 0 0 25 0 1 0 1733005218 195186688 46995 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 47653 46995 145 145 0 47508 0 [pid=13934] vsize: 190612 Current children cumulated CPU time (s) 1076.28 Current children cumulated vsize (Kb) 192736 [startup+1090.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 48746 0 0 0 108324 302 0 0 25 0 1 0 1733005218 196349952 47277 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 47937 47277 145 145 0 47792 0 [pid=13934] vsize: 191748 Current children cumulated CPU time (s) 1086.26 Current children cumulated vsize (Kb) 193872 [startup+1100.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 49025 0 0 0 109320 303 0 0 25 0 1 0 1733005218 197492736 47556 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 48216 47556 145 145 0 48071 0 [pid=13934] vsize: 192864 Current children cumulated CPU time (s) 1096.23 Current children cumulated vsize (Kb) 194988 [startup+1110.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 49311 0 0 0 110316 304 0 0 25 0 1 0 1733005218 198660096 47842 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 48501 47842 145 145 0 48356 0 [pid=13934] vsize: 194004 Current children cumulated CPU time (s) 1106.2 Current children cumulated vsize (Kb) 196128 [startup+1120.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 49589 0 0 0 111312 306 0 0 25 0 1 0 1733005218 199798784 48120 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 48779 48120 145 145 0 48634 0 [pid=13934] vsize: 195116 Current children cumulated CPU time (s) 1116.18 Current children cumulated vsize (Kb) 197240 [startup+1130.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 49890 0 0 0 112307 308 0 0 25 0 1 0 1733005218 201027584 48421 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 49079 48421 145 145 0 48934 0 [pid=13934] vsize: 196316 Current children cumulated CPU time (s) 1126.15 Current children cumulated vsize (Kb) 198440 [startup+1140.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 50221 0 0 0 113303 310 0 0 25 0 1 0 1733005218 202379264 48752 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 49409 48752 145 145 0 49264 0 [pid=13934] vsize: 197636 Current children cumulated CPU time (s) 1136.13 Current children cumulated vsize (Kb) 199760 [startup+1150.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 50589 0 0 0 114298 312 0 0 25 0 1 0 1733005218 203886592 49120 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 49777 49120 145 145 0 49632 0 [pid=13934] vsize: 199108 Current children cumulated CPU time (s) 1146.1 Current children cumulated vsize (Kb) 201232 [startup+1160.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 50927 0 0 0 115295 313 0 0 25 0 1 0 1733005218 205271040 49458 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 50115 49458 145 145 0 49970 0 [pid=13934] vsize: 200460 Current children cumulated CPU time (s) 1156.08 Current children cumulated vsize (Kb) 202584 [startup+1170.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 51229 0 0 0 116291 316 0 0 25 0 1 0 1733005218 206503936 49760 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 50416 49760 145 145 0 50271 0 [pid=13934] vsize: 201664 Current children cumulated CPU time (s) 1166.07 Current children cumulated vsize (Kb) 203788 [startup+1180.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13934 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 51569 0 0 0 117286 318 0 0 25 0 1 0 1733005218 207892480 50100 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 50755 50100 145 145 0 50610 0 [pid=13934] vsize: 203020 Current children cumulated CPU time (s) 1176.04 Current children cumulated vsize (Kb) 205144 [startup+1190.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13936 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 51859 0 0 0 118281 321 0 0 25 0 1 0 1733005218 209072128 50390 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 51043 50390 145 145 0 50898 0 [pid=13934] vsize: 204172 Current children cumulated CPU time (s) 1186.02 Current children cumulated vsize (Kb) 206296 [startup+1200.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13936 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 52154 0 0 0 119277 323 0 0 25 0 1 0 1733005218 210280448 50685 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 51338 50685 145 145 0 51193 0 [pid=13934] vsize: 205352 Current children cumulated CPU time (s) 1196 Current children cumulated vsize (Kb) 207476 [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13936 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 52440 0 0 0 120273 325 0 0 25 0 1 0 1733005218 211443712 50971 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 51622 50971 145 145 0 51477 0 [pid=13934] vsize: 206488 Current children cumulated CPU time (s) 1205.98 Current children cumulated vsize (Kb) 208612 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/58 13936 Raw data (/proc/13930/stat): 13930 (minisat+_script) S 13929 13930 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1733005213 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13930/statm): 531 226 485 147 0 384 0 [pid=13930] vsize: 2124 Raw data (/proc/13934/stat): 13934 (minisat+_64-bit) R 13930 13930 20602 0 -1 0 52440 0 0 0 120273 325 0 0 25 0 1 0 1733005218 211443712 50971 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13934/statm): 51622 50971 145 145 0 51477 0 [pid=13934] vsize: 206488 Current children cumulated CPU time (s) 1205.98 Current children cumulated vsize (Kb) 208612 Sending SIGTERM to -13930 Sleeping 2 seconds One traced child (pid=13930) ended because it received signal 15 (SIGTERM) One traced child (pid=13934) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.17 CPU time (s): 1206.08 CPU user time (s): 1202.73 CPU system time (s): 3.35149 CPU usage (%): 99.6623 Max. virtual memory (cumulated for all children) (Kb): 208612
ERROR: no interpretation found !