Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-egout.opb |
MD5SUM | 9f6abccf92594d7ee18b1409c45097d3 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 471047168 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 1615 |
Biggest coefficient in the objective function | 545997717504 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 15186728411329 |
Number of bits of the sum of numbers in the objective function | 44 |
Biggest number in a constraint | 545997717504 |
Number of bits of the biggest number in a constraint | 39 |
Biggest sum of numbers in a constraint | 15186728411329 |
Number of bits of the biggest sum of numbers | 44 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 1118.41 |
Number of variables | 1705 |
Total number of constraints | 153 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 55 |
Number of constraints which are nor clauses,nor cardinality constraints | 98 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 420 |
LAUNCH ON wulflinc26 THE 2005-09-19 03:05:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2851 boxname=wulflinc26 idbench=507 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9f6abccf92594d7ee18b1409c45097d3 /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-egout.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-egout.opb IDLAUNCH: 2851 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 890384 kB Buffers: 37936 kB Cached: 78020 kB SwapCached: 868 kB Active: 69384 kB Inactive: 49244 kB HighTotal: 131008 kB HighFree: 50232 kB LowTotal: 903652 kB LowFree: 840152 kB SwapTotal: 2097892 kB SwapFree: 2096540 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 20164 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:24:19 (client local time) WITH STATUS 30 IN 1118.41 SECONDS stats: 2851 0 1118.41 30
c Parsing PB file... c Converting 115 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ########################### c -- Clauses(.)/Splits(s): (none) c ---[ 113]---> Adder-cost: 339 maxlim: 107520 bits: 18/17 c ---[ 111]---> BDD-cost: 55 c ---[ 109]---> BDD-cost: 34 c ---[ 107]---> BDD-cost: 60 c ---[ 105]---> BDD-cost: 110 c ---[ 101]---> BDD-cost: 48 c ---[ 99]---> BDD-cost: 127 c ---[ 97]---> BDD-cost: 43 c ---[ 91]---> BDD-cost: 70 c ---[ 89]---> BDD-cost: 49 c ---[ 85]---> BDD-cost: 155 c ---[ 83]---> BDD-cost: 49 c ---[ 81]---> BDD-cost: 139 c ---[ 79]---> BDD-cost: 58 c ---[ 75]---> BDD-cost: 60 c ---[ 73]---> BDD-cost: 37 c ---[ 71]---> Sorter-cost: 634 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> BDD-cost: 70 c ---[ 67]---> Sorter-cost: 363 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> BDD-cost: 145 c ---[ 59]---> BDD-cost: 60 c ---[ 57]---> BDD-cost: 49 c ---[ 55]---> BDD-cost: 49 c ---[ 53]---> BDD-cost: 60 c ---[ 49]---> Sorter-cost: 381 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 381 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> BDD-cost: 58 c ---[ 44]---> BDD-cost: 12 c ---[ 43]---> BDD-cost: 12 c ---[ 42]---> BDD-cost: 12 c ---[ 41]---> BDD-cost: 13 c ---[ 40]---> BDD-cost: 13 c ---[ 39]---> BDD-cost: 14 c ---[ 37]---> BDD-cost: 15 c ---[ 36]---> BDD-cost: 15 c ---[ 35]---> BDD-cost: 15 c ---[ 34]---> BDD-cost: 15 c ---[ 31]---> BDD-cost: 15 c ---[ 30]---> BDD-cost: 15 c ---[ 29]---> BDD-cost: 16 c ---[ 27]---> BDD-cost: 31 c ---[ 26]---> BDD-cost: 31 c ---[ 25]---> BDD-cost: 31 c ---[ 24]---> BDD-cost: 31 c ---[ 23]---> BDD-cost: 31 c ---[ 21]---> BDD-cost: 13 c ---[ 20]---> BDD-cost: 13 c ---[ 19]---> BDD-cost: 13 c ---[ 18]---> BDD-cost: 31 c ---[ 17]---> BDD-cost: 31 c ---[ 16]---> BDD-cost: 15 c ---[ 15]---> BDD-cost: 15 c ---[ 14]---> BDD-cost: 31 c ---[ 13]---> BDD-cost: 31 c ---[ 12]---> BDD-cost: 31 c ---[ 9]---> BDD-cost: 31 c ---[ 8]---> BDD-cost: 31 c ---[ 7]---> BDD-cost: 31 c ---[ 6]---> BDD-cost: 31 c ---[ 4]---> BDD-cost: 31 c ---[ 3]---> BDD-cost: 31 c ---[ 2]---> BDD-cost: 31 c ---[ 1]---> BDD-cost: 31 c ---[ 0]---> BDD-cost: 31 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11092 29500 | 3697 0 0 nan | 0.000 % | c | 100 | 10818 28827 | 4066 63 280 4.4 | 27.106 % | c | 250 | 10461 28046 | 4473 152 576 3.8 | 29.335 % | c | 475 | 10435 27992 | 4920 367 2302 6.3 | 29.543 % | c ============================================================================== c [1mFound solution: 790136183[0m c ---[ 0]---> Sorter-cost:116869 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 551 | 342702 803652 | 114234 434 2916 6.7 | 29.543 % | c | 651 | 342649 803542 | 125657 517 3370 6.5 | 1.374 % | c | 801 | 342492 803212 | 138223 614 4825 7.9 | 1.429 % | c | 1026 | 342462 803152 | 152045 824 6926 8.4 | 1.442 % | c | 1365 | 342462 803152 | 167249 1163 10178 8.8 | 1.442 % | c | 1871 | 342448 803121 | 183974 1667 14953 9.0 | 1.445 % | c ============================================================================== c [1mFound solution: 787836070[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2031 | 343541 806548 | 114513 1821 20102 11.0 | 1.445 % | c | 2131 | 342381 803940 | 125964 1912 21570 11.3 | 1.712 % | c ============================================================================== c [1mFound solution: 641849380[0m c ---[ 0]---> Sorter-cost:54320 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2200 | 491103 1151289 | 163701 1978 22839 11.5 | 1.712 % | c | 2300 | 491051 1151173 | 180071 2076 23686 11.4 | 1.239 % | c | 2450 | 485688 1139024 | 198078 2186 25750 11.8 | 2.142 % | c | 2675 | 484954 1137363 | 217886 2402 33244 13.8 | 2.268 % | c | 3013 | 479071 1123907 | 239674 2728 63648 23.3 | 3.322 % | c | 3519 | 479036 1123826 | 263642 3233 70618 21.8 | 3.330 % | c | 4278 | 477156 1119563 | 290006 3971 97970 24.7 | 3.632 % | c | 5417 | 476951 1119096 | 319006 5103 229500 45.0 | 3.670 % | c | 7125 | 475968 1116840 | 350907 6802 281414 41.4 | 3.841 % | c ============================================================================== c [1mFound solution: 641510112[0m c ---[ 0]---> Sorter-cost:57305 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7236 | 635245 1488680 | 211748 6913 282937 40.9 | 3.841 % | c | 7337 | 635245 1488680 | 232922 7014 296309 42.2 | 3.021 % | c | 7488 | 635176 1488526 | 256215 7160 304834 42.6 | 3.034 % | c | 7713 | 635176 1488526 | 281836 7385 311292 42.2 | 3.034 % | c | 8050 | 634959 1488029 | 310020 7721 317236 41.1 | 3.064 % | c | 8558 | 634959 1488029 | 341022 8229 326912 39.7 | 3.064 % | c | 9317 | 634959 1488029 | 375124 8988 385949 42.9 | 3.064 % | c ============================================================================== c [1mFound solution: 631308145[0m c ---[ 0]---> Sorter-cost: 25 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9517 | 634993 1488681 | 211664 9188 397359 43.2 | 3.064 % | c | 9617 | 634993 1488681 | 232830 9288 398829 42.9 | 3.064 % | c | 9767 | 634993 1488681 | 256113 9438 399924 42.4 | 3.064 % | c | 9992 | 634993 1488681 | 281724 9663 402008 41.6 | 3.064 % | c | 10329 | 634993 1488681 | 309897 10000 405040 40.5 | 3.064 % | c | 10835 | 634976 1488644 | 340886 10505 408311 38.9 | 3.067 % | c | 11594 | 634976 1488644 | 374975 11264 440595 39.1 | 3.067 % | c ============================================================================== c [1mFound solution: 629990536[0m c ---[ 0]---> Sorter-cost: 22 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12067 | 635197 1489236 | 211732 11733 462718 39.4 | 3.067 % | c ============================================================================== c [1mFound solution: 629989990[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12068 | 635217 1489286 | 211739 11734 462725 39.4 | 3.067 % | c ============================================================================== c [1mFound solution: 629987824[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12071 | 635242 1489346 | 211747 11737 463826 39.5 | 3.067 % | c | 12171 | 634779 1488310 | 232921 11816 466306 39.5 | 3.149 % | c | 12321 | 634711 1488158 | 256213 11965 467610 39.1 | 3.157 % | c ============================================================================== c [1mFound solution: 625743872[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12524 | 635128 1489179 | 211709 12166 476578 39.2 | 3.157 % | c | 12626 | 634997 1488887 | 232879 12267 477513 38.9 | 3.172 % | c | 12776 | 634932 1488741 | 256167 12415 479453 38.6 | 3.181 % | c | 13003 | 634932 1488741 | 281784 12642 481401 38.1 | 3.181 % | c ============================================================================== c [1mFound solution: 527555584[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13127 | 634757 1488439 | 211585 12765 482939 37.8 | 3.181 % | c | 13227 | 634757 1488439 | 232743 12865 489477 38.0 | 3.217 % | c ============================================================================== c [1mFound solution: 519630848[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13261 | 634750 1488429 | 211583 12897 489902 38.0 | 3.217 % | c | 13361 | 634750 1488429 | 232741 12997 493944 38.0 | 3.221 % | c | 13513 | 634746 1488420 | 256015 13146 495485 37.7 | 3.222 % | c | 13738 | 634619 1488130 | 281616 13369 526009 39.3 | 3.237 % | c ============================================================================== c [1mFound solution: 516612560[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13936 | 634646 1488191 | 211548 13567 537238 39.6 | 3.237 % | c | 14039 | 634646 1488191 | 232702 13670 543759 39.8 | 3.237 % | c | 14189 | 634646 1488191 | 255973 13820 555383 40.2 | 3.237 % | c | 14419 | 634469 1487800 | 281570 14042 560233 39.9 | 3.263 % | c | 14756 | 634469 1487800 | 309727 14379 581027 40.4 | 3.263 % | c | 15263 | 634399 1487640 | 340700 14881 597600 40.2 | 3.273 % | c | 16022 | 634210 1487217 | 374770 15639 649030 41.5 | 3.296 % | c | 17162 | 632880 1484200 | 412247 16715 728206 43.6 | 3.473 % | c ============================================================================== c [1mFound solution: 515807136[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17646 | 632902 1484251 | 210967 17199 796539 46.3 | 3.473 % | c | 17748 | 632902 1484251 | 232063 17301 805371 46.6 | 3.473 % | c | 17898 | 632902 1484251 | 255270 17451 808224 46.3 | 3.473 % | c | 18123 | 632902 1484251 | 280797 17676 820943 46.4 | 3.473 % | c ============================================================================== c [1mFound solution: 515620864[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18234 | 632917 1484284 | 210972 17787 827395 46.5 | 3.473 % | c | 18336 | 632917 1484284 | 232069 17889 829065 46.3 | 3.473 % | c | 18487 | 632917 1484284 | 255276 18040 832126 46.1 | 3.474 % | c | 18712 | 632917 1484284 | 280803 18265 835541 45.7 | 3.473 % | c | 19049 | 632917 1484284 | 308884 18602 843674 45.4 | 3.474 % | c | 19555 | 632831 1484093 | 339772 18339 866385 47.2 | 3.486 % | c ============================================================================== c [1mFound solution: 512361472[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19977 | 632764 1483950 | 210921 18757 880688 47.0 | 3.486 % | c | 20078 | 632743 1483903 | 232013 18852 882296 46.8 | 3.504 % | c | 20229 | 632743 1483903 | 255214 19003 886606 46.7 | 3.504 % | c | 20454 | 632743 1483903 | 280735 19228 896523 46.6 | 3.504 % | c | 20791 | 632462 1483267 | 308809 19558 915667 46.8 | 3.539 % | c | 21300 | 632462 1483267 | 339690 20067 967402 48.2 | 3.539 % | c ============================================================================== c [1mFound solution: 494220288[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21941 | 632461 1483270 | 210820 20703 1008230 48.7 | 3.539 % | c | 22041 | 632461 1483270 | 231902 20803 1020378 49.0 | 3.543 % | c ============================================================================== c [1mFound solution: 493697024[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22104 | 632479 1483316 | 210826 20866 1021877 49.0 | 3.543 % | c | 22204 | 632479 1483316 | 231908 20966 1024945 48.9 | 3.544 % | c | 22355 | 632479 1483316 | 255099 21117 1034835 49.0 | 3.544 % | c | 22580 | 632479 1483316 | 280609 21342 1041324 48.8 | 3.544 % | c | 22918 | 632479 1483316 | 308670 21680 1055245 48.7 | 3.544 % | c | 23424 | 632479 1483316 | 339537 22186 1098345 49.5 | 3.544 % | c | 24186 | 632479 1483316 | 373491 22948 1155521 50.4 | 3.544 % | c ============================================================================== c [1mFound solution: 493501312[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24928 | 632501 1483368 | 210833 23690 1189701 50.2 | 3.544 % | c | 25028 | 632501 1483368 | 231916 23790 1196652 50.3 | 3.544 % | c | 25180 | 632501 1483368 | 255107 23942 1205144 50.3 | 3.544 % | c | 25407 | 632501 1483368 | 280618 24169 1211295 50.1 | 3.544 % | c | 25745 | 632501 1483368 | 308680 24507 1240119 50.6 | 3.544 % | c ============================================================================== c [1mFound solution: 489304064[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26109 | 632517 1483405 | 210839 24871 1267828 51.0 | 3.544 % | c | 26209 | 632517 1483405 | 231922 24971 1276605 51.1 | 3.544 % | c | 26359 | 632517 1483405 | 255115 25121 1282518 51.1 | 3.544 % | c | 26586 | 632517 1483405 | 280626 25348 1292110 51.0 | 3.544 % | c | 26923 | 632517 1483405 | 308689 25685 1303287 50.7 | 3.544 % | c | 27430 | 632517 1483405 | 339558 26192 1325978 50.6 | 3.544 % | c ============================================================================== c [1mFound solution: 488373248[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27516 | 632532 1483441 | 210844 26278 1329979 50.6 | 3.544 % | c | 27616 | 632532 1483441 | 231928 26378 1334243 50.6 | 3.545 % | c | 27766 | 632381 1483099 | 255121 26527 1347432 50.8 | 3.563 % | c | 27991 | 632381 1483099 | 280633 26752 1359555 50.8 | 3.563 % | c ============================================================================== c [1mFound solution: 482404352[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28296 | 632403 1483154 | 210801 27057 1382197 51.1 | 3.563 % | c | 28396 | 632403 1483154 | 231881 27157 1384666 51.0 | 3.563 % | c ============================================================================== c [1mFound solution: 480050176[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28404 | 632412 1483180 | 210804 27165 1384862 51.0 | 3.563 % | c | 28507 | 632412 1483180 | 231884 27268 1387112 50.9 | 3.563 % | c | 28658 | 632412 1483180 | 255072 27419 1390731 50.7 | 3.563 % | c ============================================================================== c [1mFound solution: 474212352[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28663 | 632424 1483207 | 210808 27424 1390964 50.7 | 3.563 % | c | 28763 | 632424 1483207 | 231888 27524 1393092 50.6 | 3.563 % | c | 28913 | 632424 1483207 | 255077 27674 1397868 50.5 | 3.563 % | c | 29138 | 632424 1483207 | 280585 27899 1402701 50.3 | 3.563 % | c | 29475 | 632424 1483207 | 308643 28236 1410024 49.9 | 3.563 % | c | 29981 | 632424 1483207 | 339508 28742 1424166 49.5 | 3.563 % | c | 30740 | 632424 1483207 | 373459 29501 1443029 48.9 | 3.563 % | c ============================================================================== c [1mFound solution: 473361408[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31450 | 632442 1483249 | 210814 30211 1472693 48.7 | 3.563 % | c | 31552 | 632442 1483249 | 231895 30313 1475203 48.7 | 3.564 % | c ============================================================================== c [1mFound solution: 471047168[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31617 | 632454 1483278 | 210818 30378 1477273 48.6 | 3.564 % | c | 31720 | 632454 1483278 | 231899 30481 1482311 48.6 | 3.564 % | c | 31870 | 632454 1483278 | 255089 30631 1487267 48.6 | 3.564 % | c | 32097 | 632454 1483278 | 280598 30858 1495234 48.5 | 3.564 % | c | 32435 | 632454 1483278 | 308658 31196 1507843 48.3 | 3.564 % | c | 32942 | 632454 1483278 | 339524 31703 1527516 48.2 | 3.564 % | c | 33701 | 632454 1483278 | 373476 32462 1558062 48.0 | 3.564 % | c | 34841 | 632454 1483278 | 410824 33602 1594606 47.5 | 3.564 % | c ============================================================================== c [1mOptimal solution: 471047168[0m s OPTIMUM FOUND v I_0x2e_001_0x2e__0x2e__0x2e__bit0 -I_0x2e_001003_bit0 -I_0x2e_002003_bit0 -I_0x2e_002_0x2e__0x2e__0x2e__bit0 -I_0x2e_003005_bit0 I_0x2e_004005_bit0 -I_0x2e_004_0x2e__0x2e__0x2e__bit0 I_0x2e_005007_bit0 I_0x2e_006007_bit0 I_0x2e_007008_bit0 I_0x2e_008_0x2e__0x2e__0x2e__bit0 -I_0x2e_008009_bit0 I_0x2e_010012_bit0 I_0x2e_011012_bit0 -I_0x2e_012_0x2e__0x2e__0x2e__bit0 I_0x2e_012013_bit0 I_0x2e_013016_bit0 -I_0x2e_014015_bit0 I_0x2e_015016_bit0 I_0x2e_016_0x2e__0x2e__0x2e__bit0 -I_0x2e_016017_bit0 -I_0x2e_017018_bit0 -I_0x2e_009018_bit0 -I_0x2e_018019_bit0 I_0x2e_019024_bit0 -I_0x2e_024_0x2e__0x2e__0x2e__bit0 -I_0x2e_023024_bit0 -I_0x2e_022023_bit0 -I_0x2e_020022_bit0 I_0x2e_021022_bit0 I_0x2e_022_0x2e__0x2e__0x2e__bit0 I_0x2e_024026_bit0 I_0x2e_025026_bit0 -I_0x2e_025_0x2e__0x2e__0x2e__bit0 I_0x2e_026027_bit0 -I_0x2e_027_0x2e__0x2e__0x2e__bit0 I_0x2e_027032_bit0 -I_0x2e_030031_bit0 I_0x2e_031032_bit0 I_0x2e_029031_bit0 -I_0x2e_028029_bit0 -I_0x2e_028_0x2e__0x2e__0x2e__bit0 I_0x2e_032033_bit0 I_0x2e_033037_bit0 -I_0x2e_036037_bit0 -I_0x2e_034036_bit0 -I_0x2e_035036_bit0 I_0x2e_037038_bit0 I_0x2e_038040_bit0 I_0x2e_039040_bit0 -I_0x2e_040_0x2e__0x2e__0x2e__bit0 -I_0x2e_041_0x2e__0x2e__0x2e__bit0 I_0x2e_040041_bit0 I_0x2e_041042_bit0 I_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_001_0x2e__0x2e__0x2e__bit_10 -F_0x2e_001_0x2e__0x2e__0x2e__bit_9 -F_0x2e_001_0x2e__0x2e__0x2e__bit_8 -F_0x2e_001_0x2e__0x2e__0x2e__bit_7 -F_0x2e_001_0x2e__0x2e__0x2e__bit_6 -F_0x2e_001_0x2e__0x2e__0x2e__bit_5 -F_0x2e_001_0x2e__0x2e__0x2e__bit_4 -F_0x2e_001_0x2e__0x2e__0x2e__bit_3 -F_0x2e_001_0x2e__0x2e__0x2e__bit_2 -F_0x2e_001_0x2e__0x2e__0x2e__bit_1 -F_0x2e_001_0x2e__0x2e__0x2e__bit0 F_0x2e_001_0x2e__0x2e__0x2e__bit1 -F_0x2e_001_0x2e__0x2e__0x2e__bit2 -F_0x2e_001_0x2e__0x2e__0x2e__bit3 -F_0x2e_001_0x2e__0x2e__0x2e__bit4 -F_0x2e_001_0x2e__0x2e__0x2e__bit5 -F_0x2e_001_0x2e__0x2e__0x2e__bit6 -F_0x2e_001_0x2e__0x2e__0x2e__bit7 -F_0x2e_001_0x2e__0x2e__0x2e__bit8 -F_0x2e_001_0x2e__0x2e__0x2e__bit9 -F_0x2e_001_0x2e__0x2e__0x2e__bit10 -F_0x2e_001_0x2e__0x2e__0x2e__bit11 -F_0x2e_001_0x2e__0x2e__0x2e__bit12 -F_0x2e_001_0x2e__0x2e__0x2e__bit13 -F_0x2e_001_0x2e__0x2e__0x2e__bit14 -F_0x2e_001_0x2e__0x2e__0x2e__bit15 -F_0x2e_001_0x2e__0x2e__0x2e__bit16 -F_0x2e_001_0x2e__0x2e__0x2e__bit17 -F_0x2e_001_0x2e__0x2e__0x2e__bit18 -F_0x2e_001_0x2e__0x2e__0x2e__bit19 -F_0x2e_001003_bit_10 -F_0x2e_001003_bit_9 -F_0x2e_001003_bit_8 -F_0x2e_001003_bit_7 -F_0x2e_001003_bit_6 -F_0x2e_001003_bit_5 -F_0x2e_001003_bit_4 -F_0x2e_001003_bit_3 -F_0x2e_001003_bit_2 -F_0x2e_001003_bit_1 -F_0x2e_001003_bit0 -F_0x2e_001003_bit1 -F_0x2e_001003_bit2 -F_0x2e_001003_bit3 -F_0x2e_001003_bit4 -F_0x2e_001003_bit5 -F_0x2e_001003_bit6 -F_0x2e_001003_bit7 -F_0x2e_001003_bit8 -F_0x2e_001003_bit9 -F_0x2e_001003_bit10 -F_0x2e_001003_bit11 -F_0x2e_001003_bit12 -F_0x2e_001003_bit13 -F_0x2e_001003_bit14 -F_0x2e_001003_bit15 -F_0x2e_001003_bit16 -F_0x2e_001003_bit17 -F_0x2e_001003_bit18 -F_0x2e_001003_bit19 -F_0x2e_002003_bit_10 -F_0x2e_002003_bit_9 -F_0x2e_002003_bit_8 -F_0x2e_002003_bit_7 -F_0x2e_002003_bit_6 -F_0x2e_002003_bit_5 -F_0x2e_002003_bit_4 -F_0x2e_002003_bit_3 -F_0x2e_002003_bit_2 -F_0x2e_002003_bit_1 -F_0x2e_002003_bit0 -F_0x2e_002003_bit1 -F_0x2e_002003_bit2 -F_0x2e_002003_bit3 -F_0x2e_002003_bit4 -F_0x2e_002003_bit5 -F_0x2e_002003_bit6 -F_0x2e_002003_bit7 -F_0x2e_002003_bit8 -F_0x2e_002003_bit9 -F_0x2e_002003_bit10 -F_0x2e_002003_bit11 -F_0x2e_002003_bit12 -F_0x2e_002003_bit13 -F_0x2e_002003_bit14 -F_0x2e_002003_bit15 -F_0x2e_002003_bit16 -F_0x2e_002003_bit17 -F_0x2e_002003_bit18 -F_0x2e_002003_bit19 -F_0x2e_002_0x2e__0x2e__0x2e__bit_10 -F_0x2e_002_0x2e__0x2e__0x2e__bit_9 -F_0x2e_002_0x2e__0x2e__0x2e__bit_8 -F_0x2e_002_0x2e__0x2e__0x2e__bit_7 -F_0x2e_002_0x2e__0x2e__0x2e__bit_6 -F_0x2e_002_0x2e__0x2e__0x2e__bit_5 -F_0x2e_002_0x2e__0x2e__0x2e__bit_4 -F_0x2e_002_0x2e__0x2e__0x2e__bit_3 -F_0x2e_002_0x2e__0x2e__0x2e__bit_2 -F_0x2e_002_0x2e__0x2e__0x2e__bit_1 -F_0x2e_002_0x2e__0x2e__0x2e__bit0 -F_0x2e_002_0x2e__0x2e__0x2e__bit1 -F_0x2e_002_0x2e__0x2e__0x2e__bit2 -F_0x2e_002_0x2e__0x2e__0x2e__bit3 -F_0x2e_002_0x2e__0x2e__0x2e__bit4 -F_0x2e_002_0x2e__0x2e__0x2e__bit5 -F_0x2e_002_0x2e__0x2e__0x2e__bit6 -F_0x2e_002_0x2e__0x2e__0x2e__bit7 -F_0x2e_002_0x2e__0x2e__0x2e__bit8 -F_0x2e_002_0x2e__0x2e__0x2e__bit9 -F_0x2e_002_0x2e__0x2e__0x2e__bit10 -F_0x2e_002_0x2e__0x2e__0x2e__bit11 -F_0x2e_002_0x2e__0x2e__0x2e__bit12 -F_0x2e_002_0x2e__0x2e__0x2e__bit13 -F_0x2e_002_0x2e__0x2e__0x2e__bit14 -F_0x2e_002_0x2e__0x2e__0x2e__bit15 -F_0x2e_002_0x2e__0x2e__0x2e__bit16 -F_0x2e_002_0x2e__0x2e__0x2e__bit17 -F_0x2e_002_0x2e__0x2e__0x2e__bit18 -F_0x2e_002_0x2e__0x2e__0x2e__bit19 -F_0x2e_003005_bit_10 -F_0x2e_003005_bit_9 -F_0x2e_003005_bit_8 -F_0x2e_003005_bit_7 -F_0x2e_003005_bit_6 -F_0x2e_003005_bit_5 -F_0x2e_003005_bit_4 -F_0x2e_003005_bit_3 -F_0x2e_003005_bit_2 -F_0x2e_003005_bit_1 -F_0x2e_003005_bit0 -F_0x2e_003005_bit1 -F_0x2e_003005_bit2 -F_0x2e_003005_bit3 -F_0x2e_003005_bit4 -F_0x2e_003005_bit5 -F_0x2e_003005_bit6 -F_0x2e_003005_bit7 -F_0x2e_003005_bit8 -F_0x2e_003005_bit9 -F_0x2e_003005_bit10 -F_0x2e_003005_bit11 -F_0x2e_003005_bit12 -F_0x2e_003005_bit13 -F_0x2e_003005_bit14 -F_0x2e_003005_bit15 -F_0x2e_003005_bit16 -F_0x2e_003005_bit17 -F_0x2e_003005_bit18 -F_0x2e_003005_bit19 -F_0x2e_004005_bit_10 -F_0x2e_004005_bit_9 -F_0x2e_004005_bit_8 -F_0x2e_004005_bit_7 -F_0x2e_004005_bit_6 -F_0x2e_004005_bit_5 -F_0x2e_004005_bit_4 -F_0x2e_004005_bit_3 -F_0x2e_004005_bit_2 -F_0x2e_004005_bit_1 F_0x2e_004005_bit0 F_0x2e_004005_bit1 F_0x2e_004005_bit2 -F_0x2e_004005_bit3 -F_0x2e_004005_bit4 -F_0x2e_004005_bit5 -F_0x2e_004005_bit6 -F_0x2e_004005_bit7 -F_0x2e_004005_bit8 -F_0x2e_004005_bit9 -F_0x2e_004005_bit10 -F_0x2e_004005_bit11 -F_0x2e_004005_bit12 -F_0x2e_004005_bit13 -F_0x2e_004005_bit14 -F_0x2e_004005_bit15 -F_0x2e_004005_bit16 -F_0x2e_004005_bit17 -F_0x2e_004005_bit18 -F_0x2e_004005_bit19 -F_0x2e_004_0x2e__0x2e__0x2e__bit_10 -F_0x2e_004_0x2e__0x2e__0x2e__bit_9 -F_0x2e_004_0x2e__0x2e__0x2e__bit_8 -F_0x2e_004_0x2e__0x2e__0x2e__bit_7 -F_0x2e_004_0x2e__0x2e__0x2e__bit_6 -F_0x2e_004_0x2e__0x2e__0x2e__bit_5 -F_0x2e_004_0x2e__0x2e__0x2e__bit_4 -F_0x2e_004_0x2e__0x2e__0x2e__bit_3 -F_0x2e_004_0x2e__0x2e__0x2e__bit_2 -F_0x2e_004_0x2e__0x2e__0x2e__bit_1 -F_0x2e_004_0x2e__0x2e__0x2e__bit0 -F_0x2e_004_0x2e__0x2e__0x2e__bit1 -F_0x2e_004_0x2e__0x2e__0x2e__bit2 -F_0x2e_004_0x2e__0x2e__0x2e__bit3 -F_0x2e_004_0x2e__0x2e__0x2e__bit4 -F_0x2e_004_0x2e__0x2e__0x2e__bit5 -F_0x2e_004_0x2e__0x2e__0x2e__bit6 -F_0x2e_004_0x2e__0x2e__0x2e__bit7 -F_0x2e_004_0x2e__0x2e__0x2e__bit8 -F_0x2e_004_0x2e__0x2e__0x2e__bit9 -F_0x2e_004_0x2e__0x2e__0x2e__bit10 -F_0x2e_004_0x2e__0x2e__0x2e__bit11 -F_0x2e_004_0x2e__0x2e__0x2e__bit12 -F_0x2e_004_0x2e__0x2e__0x2e__bit13 -F_0x2e_004_0x2e__0x2e__0x2e__bit14 -F_0x2e_004_0x2e__0x2e__0x2e__bit15 -F_0x2e_004_0x2e__0x2e__0x2e__bit16 -F_0x2e_004_0x2e__0x2e__0x2e__bit17 -F_0x2e_004_0x2e__0x2e__0x2e__bit18 -F_0x2e_004_0x2e__0x2e__0x2e__bit19 -F_0x2e_005007_bit_10 -F_0x2e_005007_bit_9 -F_0x2e_005007_bit_8 -F_0x2e_005007_bit_7 -F_0x2e_005007_bit_6 -F_0x2e_005007_bit_5 -F_0x2e_005007_bit_4 -F_0x2e_005007_bit_3 -F_0x2e_005007_bit_2 -F_0x2e_005007_bit_1 F_0x2e_005007_bit0 F_0x2e_005007_bit1 F_0x2e_005007_bit2 -F_0x2e_005007_bit3 -F_0x2e_005007_bit4 -F_0x2e_005007_bit5 -F_0x2e_005007_bit6 -F_0x2e_005007_bit7 -F_0x2e_005007_bit8 -F_0x2e_005007_bit9 -F_0x2e_005007_bit10 -F_0x2e_005007_bit11 -F_0x2e_005007_bit12 -F_0x2e_005007_bit13 -F_0x2e_005007_bit14 -F_0x2e_005007_bit15 -F_0x2e_005007_bit16 -F_0x2e_005007_bit17 -F_0x2e_005007_bit18 -F_0x2e_005007_bit19 -F_0x2e_006007_bit_10 -F_0x2e_006007_bit_9 -F_0x2e_006007_bit_8 -F_0x2e_006007_bit_7 -F_0x2e_006007_bit_6 -F_0x2e_006007_bit_5 -F_0x2e_006007_bit_4 -F_0x2e_006007_bit_3 -F_0x2e_006007_bit_2 -F_0x2e_006007_bit_1 -F_0x2e_006007_bit0 -F_0x2e_006007_bit1 F_0x2e_006007_bit2 -F_0x2e_006007_bit3 -F_0x2e_006007_bit4 -F_0x2e_006007_bit5 -F_0x2e_006007_bit6 -F_0x2e_006007_bit7 -F_0x2e_006007_bit8 -F_0x2e_006007_bit9 -F_0x2e_006007_bit10 -F_0x2e_006007_bit11 -F_0x2e_006007_bit12 -F_0x2e_006007_bit13 -F_0x2e_006007_bit14 -F_0x2e_006007_bit15 -F_0x2e_006007_bit16 -F_0x2e_006007_bit17 -F_0x2e_006007_bit18 -F_0x2e_006007_bit19 -F_0x2e_007008_bit_10 -F_0x2e_007008_bit_9 -F_0x2e_007008_bit_8 -F_0x2e_007008_bit_7 -F_0x2e_007008_bit_6 -F_0x2e_007008_bit_5 -F_0x2e_007008_bit_4 -F_0x2e_007008_bit_3 -F_0x2e_007008_bit_2 -F_0x2e_007008_bit_1 -F_0x2e_007008_bit0 -F_0x2e_007008_bit1 F_0x2e_007008_bit2 F_0x2e_007008_bit3 -F_0x2e_007008_bit4 -F_0x2e_007008_bit5 -F_0x2e_007008_bit6 -F_0x2e_007008_bit7 -F_0x2e_007008_bit8 -F_0x2e_007008_bit9 -F_0x2e_007008_bit10 -F_0x2e_007008_bit11 -F_0x2e_007008_bit12 -F_0x2e_007008_bit13 -F_0x2e_007008_bit14 -F_0x2e_007008_bit15 -F_0x2e_007008_bit16 -F_0x2e_007008_bit17 -F_0x2e_007008_bit18 -F_0x2e_007008_bit19 -F_0x2e_008_0x2e__0x2e__0x2e__bit_10 -F_0x2e_008_0x2e__0x2e__0x2e__bit_9 -F_0x2e_008_0x2e__0x2e__0x2e__bit_8 -F_0x2e_008_0x2e__0x2e__0x2e__bit_7 -F_0x2e_008_0x2e__0x2e__0x2e__bit_6 -F_0x2e_008_0x2e__0x2e__0x2e__bit_5 -F_0x2e_008_0x2e__0x2e__0x2e__bit_4 -F_0x2e_008_0x2e__0x2e__0x2e__bit_3 -F_0x2e_008_0x2e__0x2e__0x2e__bit_2 -F_0x2e_008_0x2e__0x2e__0x2e__bit_1 -F_0x2e_008_0x2e__0x2e__0x2e__bit0 -F_0x2e_008_0x2e__0x2e__0x2e__bit1 F_0x2e_008_0x2e__0x2e__0x2e__bit2 F_0x2e_008_0x2e__0x2e__0x2e__bit3 -F_0x2e_008_0x2e__0x2e__0x2e__bit4 -F_0x2e_008_0x2e__0x2e__0x2e__bit5 -F_0x2e_008_0x2e__0x2e__0x2e__bit6 -F_0x2e_008_0x2e__0x2e__0x2e__bit7 -F_0x2e_008_0x2e__0x2e__0x2e__bit8 -F_0x2e_008_0x2e__0x2e__0x2e__bit9 -F_0x2e_008_0x2e__0x2e__0x2e__bit10 -F_0x2e_008_0x2e__0x2e__0x2e__bit11 -F_0x2e_008_0x2e__0x2e__0x2e__bit12 -F_0x2e_008_0x2e__0x2e__0x2e__bit13 -F_0x2e_008_0x2e__0x2e__0x2e__bit14 -F_0x2e_008_0x2e__0x2e__0x2e__bit15 -F_0x2e_008_0x2e__0x2e__0x2e__bit16 -F_0x2e_008_0x2e__0x2e__0x2e__bit17 -F_0x2e_008_0x2e__0x2e__0x2e__bit18 -F_0x2e_008_0x2e__0x2e__0x2e__bit19 -F_0x2e_008009_bit_10 -F_0x2e_008009_bit_9 -F_0x2e_008009_bit_8 -F_0x2e_008009_bit_7 -F_0x2e_008009_bit_6 -F_0x2e_008009_bit_5 -F_0x2e_008009_bit_4 -F_0x2e_008009_bit_3 -F_0x2e_008009_bit_2 -F_0x2e_008009_bit_1 -F_0x2e_008009_bit0 -F_0x2e_008009_bit1 -F_0x2e_008009_bit2 -F_0x2e_008009_bit3 -F_0x2e_008009_bit4 -F_0x2e_008009_bit5 -F_0x2e_008009_bit6 -F_0x2e_008009_bit7 -F_0x2e_008009_bit8 -F_0x2e_008009_bit9 -F_0x2e_008009_bit10 -F_0x2e_008009_bit11 -F_0x2e_008009_bit12 -F_0x2e_008009_bit13 -F_0x2e_008009_bit14 -F_0x2e_008009_bit15 -F_0x2e_008009_bit16 -F_0x2e_008009_bit17 -F_0x2e_008009_bit18 -F_0x2e_008009_bit19 -F_0x2e_010012_bit_10 -F_0x2e_010012_bit_9 -F_0x2e_010012_bit_8 -F_0x2e_010012_bit_7 -F_0x2e_010012_bit_6 -F_0x2e_010012_bit_5 -F_0x2e_010012_bit_4 -F_0x2e_010012_bit_3 -F_0x2e_010012_bit_2 -F_0x2e_010012_bit_1 F_0x2e_010012_bit0 -F_0x2e_010012_bit1 -F_0x2e_010012_bit2 -F_0x2e_010012_bit3 -F_0x2e_010012_bit4 -F_0x2e_010012_bit5 -F_0x2e_010012_bit6 -F_0x2e_010012_bit7 -F_0x2e_010012_bit8 -F_0x2e_010012_bit9 -F_0x2e_010012_bit10 -F_0x2e_010012_bit11 -F_0x2e_010012_bit12 -F_0x2e_010012_bit13 -F_0x2e_010012_bit14 -F_0x2e_010012_bit15 -F_0x2e_010012_bit16 -F_0x2e_010012_bit17 -F_0x2e_010012_bit18 -F_0x2e_010012_bit19 -F_0x2e_012_0x2e__0x2e__0x2e__bit_10 -F_0x2e_012_0x2e__0x2e__0x2e__bit_9 -F_0x2e_012_0x2e__0x2e__0x2e__bit_8 -F_0x2e_012_0x2e__0x2e__0x2e__bit_7 -F_0x2e_012_0x2e__0x2e__0x2e__bit_6 -F_0x2e_012_0x2e__0x2e__0x2e__bit_5 -F_0x2e_012_0x2e__0x2e__0x2e__bit_4 -F_0x2e_012_0x2e__0x2e__0x2e__bit_3 -F_0x2e_012_0x2e__0x2e__0x2e__bit_2 -F_0x2e_012_0x2e__0x2e__0x2e__bit_1 -F_0x2e_012_0x2e__0x2e__0x2e__bit0 -F_0x2e_012_0x2e__0x2e__0x2e__bit1 -F_0x2e_012_0x2e__0x2e__0x2e__bit2 -F_0x2e_012_0x2e__0x2e__0x2e__bit3 -F_0x2e_012_0x2e__0x2e__0x2e__bit4 -F_0x2e_012_0x2e__0x2e__0x2e__bit5 -F_0x2e_012_0x2e__0x2e__0x2e__bit6 -F_0x2e_012_0x2e__0x2e__0x2e__bit7 -F_0x2e_012_0x2e__0x2e__0x2e__bit8 -F_0x2e_012_0x2e__0x2e__0x2e__bit9 -F_0x2e_012_0x2e__0x2e__0x2e__bit10 -F_0x2e_012_0x2e__0x2e__0x2e__bit11 -F_0x2e_012_0x2e__0x2e__0x2e__bit12 -F_0x2e_012_0x2e__0x2e__0x2e__bit13 -F_0x2e_012_0x2e__0x2e__0x2e__bit14 -F_0x2e_012_0x2e__0x2e__0x2e__bit15 -F_0x2e_012_0x2e__0x2e__0x2e__bit16 -F_0x2e_012_0x2e__0x2e__0x2e__bit17 -F_0x2e_012_0x2e__0x2e__0x2e__bit18 -F_0x2e_012_0x2e__0x2e__0x2e__bit19 -F_0x2e_012013_bit_10 -F_0x2e_012013_bit_9 -F_0x2e_012013_bit_8 -F_0x2e_012013_bit_7 -F_0x2e_012013_bit_6 -F_0x2e_012013_bit_5 -F_0x2e_012013_bit_4 -F_0x2e_012013_bit_3 -F_0x2e_012013_bit_2 -F_0x2e_012013_bit_1 -F_0x2e_012013_bit0 F_0x2e_012013_bit1 F_0x2e_012013_bit2 -F_0x2e_012013_bit3 F_0x2e_012013_bit4 -F_0x2e_012013_bit5 -F_0x2e_012013_bit6 -F_0x2e_012013_bit7 -F_0x2e_012013_bit8 -F_0x2e_012013_bit9 -F_0x2e_012013_bit10 -F_0x2e_012013_bit11 -F_0x2e_012013_bit12 -F_0x2e_012013_bit13 -F_0x2e_012013_bit14 -F_0x2e_012013_bit15 -F_0x2e_012013_bit16 -F_0x2e_012013_bit17 -F_0x2e_012013_bit18 -F_0x2e_012013_bit19 -F_0x2e_013016_bit_10 -F_0x2e_013016_bit_9 -F_0x2e_013016_bit_8 -F_0x2e_013016_bit_7 -F_0x2e_013016_bit_6 -F_0x2e_013016_bit_5 -F_0x2e_013016_bit_4 -F_0x2e_013016_bit_3 -F_0x2e_013016_bit_2 -F_0x2e_013016_bit_1 -F_0x2e_013016_bit0 F_0x2e_013016_bit1 -F_0x2e_013016_bit2 F_0x2e_013016_bit3 F_0x2e_013016_bit4 -F_0x2e_013016_bit5 -F_0x2e_013016_bit6 -F_0x2e_013016_bit7 -F_0x2e_013016_bit8 -F_0x2e_013016_bit9 -F_0x2e_013016_bit10 -F_0x2e_013016_bit11 -F_0x2e_013016_bit12 -F_0x2e_013016_bit13 -F_0x2e_013016_bit14 -F_0x2e_013016_bit15 -F_0x2e_013016_bit16 -F_0x2e_013016_bit17 -F_0x2e_013016_bit18 -F_0x2e_013016_bit19 -F_0x2e_014015_bit_10 -F_0x2e_014015_bit_9 -F_0x2e_014015_bit_8 -F_0x2e_014015_bit_7 -F_0x2e_014015_bit_6 -F_0x2e_014015_bit_5 -F_0x2e_014015_bit_4 -F_0x2e_014015_bit_3 -F_0x2e_014015_bit_2 -F_0x2e_014015_bit_1 -F_0x2e_014015_bit0 -F_0x2e_014015_bit1 -F_0x2e_014015_bit2 -F_0x2e_014015_bit3 -F_0x2e_014015_bit4 -F_0x2e_014015_bit5 -F_0x2e_014015_bit6 -F_0x2e_014015_bit7 -F_0x2e_014015_bit8 -F_0x2e_014015_bit9 -F_0x2e_014015_bit10 -F_0x2e_014015_bit11 -F_0x2e_014015_bit12 -F_0x2e_014015_bit13 -F_0x2e_014015_bit14 -F_0x2e_014015_bit15 -F_0x2e_014015_bit16 -F_0x2e_014015_bit17 -F_0x2e_014015_bit18 -F_0x2e_014015_bit19 -F_0x2e_015016_bit_10 -F_0x2e_015016_bit_9 -F_0x2e_015016_bit_8 -F_0x2e_015016_bit_7 -F_0x2e_015016_bit_6 -F_0x2e_015016_bit_5 -F_0x2e_015016_bit_4 -F_0x2e_015016_bit_3 -F_0x2e_015016_bit_2 -F_0x2e_015016_bit_1 F_0x2e_015016_bit0 -F_0x2e_015016_bit1 -F_0x2e_015016_bit2 -F_0x2e_015016_bit3 -F_0x2e_015016_bit4 -F_0x2e_015016_bit5 -F_0x2e_015016_bit6 -F_0x2e_015016_bit7 -F_0x2e_015016_bit8 -F_0x2e_015016_bit9 -F_0x2e_015016_bit10 -F_0x2e_015016_bit11 -F_0x2e_015016_bit12 -F_0x2e_015016_bit13 -F_0x2e_015016_bit14 -F_0x2e_015016_bit15 -F_0x2e_015016_bit16 -F_0x2e_015016_bit17 -F_0x2e_015016_bit18 -F_0x2e_015016_bit19 -F_0x2e_016_0x2e__0x2e__0x2e__bit_10 -F_0x2e_016_0x2e__0x2e__0x2e__bit_9 -F_0x2e_016_0x2e__0x2e__0x2e__bit_8 -F_0x2e_016_0x2e__0x2e__0x2e__bit_7 -F_0x2e_016_0x2e__0x2e__0x2e__bit_6 -F_0x2e_016_0x2e__0x2e__0x2e__bit_5 -F_0x2e_016_0x2e__0x2e__0x2e__bit_4 -F_0x2e_016_0x2e__0x2e__0x2e__bit_3 -F_0x2e_016_0x2e__0x2e__0x2e__bit_2 -F_0x2e_016_0x2e__0x2e__0x2e__bit_1 F_0x2e_016_0x2e__0x2e__0x2e__bit0 F_0x2e_016_0x2e__0x2e__0x2e__bit1 -F_0x2e_016_0x2e__0x2e__0x2e__bit2 F_0x2e_016_0x2e__0x2e__0x2e__bit3 F_0x2e_016_0x2e__0x2e__0x2e__bit4 -F_0x2e_016_0x2e__0x2e__0x2e__bit5 -F_0x2e_016_0x2e__0x2e__0x2e__bit6 -F_0x2e_016_0x2e__0x2e__0x2e__bit7 -F_0x2e_016_0x2e__0x2e__0x2e__bit8 -F_0x2e_016_0x2e__0x2e__0x2e__bit9 -F_0x2e_016_0x2e__0x2e__0x2e__bit10 -F_0x2e_016_0x2e__0x2e__0x2e__bit11 -F_0x2e_016_0x2e__0x2e__0x2e__bit12 -F_0x2e_016_0x2e__0x2e__0x2e__bit13 -F_0x2e_016_0x2e__0x2e__0x2e__bit14 -F_0x2e_016_0x2e__0x2e__0x2e__bit15 -F_0x2e_016_0x2e__0x2e__0x2e__bit16 -F_0x2e_016_0x2e__0x2e__0x2e__bit17 -F_0x2e_016_0x2e__0x2e__0x2e__bit18 -F_0x2e_016_0x2e__0x2e__0x2e__bit19 -F_0x2e_016017_bit_10 -F_0x2e_016017_bit_9 -F_0x2e_016017_bit_8 -F_0x2e_016017_bit_7 -F_0x2e_016017_bit_6 -F_0x2e_016017_bit_5 -F_0x2e_016017_bit_4 -F_0x2e_016017_bit_3 -F_0x2e_016017_bit_2 -F_0x2e_016017_bit_1 -F_0x2e_016017_bit0 -F_0x2e_016017_bit1 -F_0x2e_016017_bit2 -F_0x2e_016017_bit3 -F_0x2e_016017_bit4 -F_0x2e_016017_bit5 -F_0x2e_016017_bit6 -F_0x2e_016017_bit7 -F_0x2e_016017_bit8 -F_0x2e_016017_bit9 -F_0x2e_016017_bit10 -F_0x2e_016017_bit11 -F_0x2e_016017_bit12 -F_0x2e_016017_bit13 -F_0x2e_016017_bit14 -F_0x2e_016017_bit15 -F_0x2e_016017_bit16 -F_0x2e_016017_bit17 -F_0x2e_016017_bit18 -F_0x2e_016017_bit19 -F_0x2e_017018_bit_10 -F_0x2e_017018_bit_9 -F_0x2e_017018_bit_8 -F_0x2e_017018_bit_7 -F_0x2e_017018_bit_6 -F_0x2e_017018_bit_5 -F_0x2e_017018_bit_4 -F_0x2e_017018_bit_3 -F_0x2e_017018_bit_2 -F_0x2e_017018_bit_1 -F_0x2e_017018_bit0 -F_0x2e_017018_bit1 -F_0x2e_017018_bit2 -F_0x2e_017018_bit3 -F_0x2e_017018_bit4 -F_0x2e_017018_bit5 -F_0x2e_017018_bit6 -F_0x2e_017018_bit7 -F_0x2e_017018_bit8 -F_0x2e_017018_bit9 -F_0x2e_017018_bit10 -F_0x2e_017018_bit11 -F_0x2e_017018_bit12 -F_0x2e_017018_bit13 -F_0x2e_017018_bit14 -F_0x2e_017018_bit15 -F_0x2e_017018_bit16 -F_0x2e_017018_bit17 -F_0x2e_017018_bit18 -F_0x2e_017018_bit19 -F_0x2e_009018_bit_10 -F_0x2e_009018_bit_9 -F_0x2e_009018_bit_8 -F_0x2e_009018_bit_7 -F_0x2e_009018_bit_6 -F_0x2e_009018_bit_5 -F_0x2e_009018_bit_4 -F_0x2e_009018_bit_3 -F_0x2e_009018_bit_2 -F_0x2e_009018_bit_1 -F_0x2e_009018_bit0 -F_0x2e_009018_bit1 -F_0x2e_009018_bit2 -F_0x2e_009018_bit3 -F_0x2e_009018_bit4 -F_0x2e_009018_bit5 -F_0x2e_009018_bit6 -F_0x2e_009018_bit7 -F_0x2e_009018_bit8 -F_0x2e_009018_bit9 -F_0x2e_009018_bit10 -F_0x2e_009018_bit11 -F_0x2e_009018_bit12 -F_0x2e_009018_bit13 -F_0x2e_009018_bit14 -F_0x2e_009018_bit15 -F_0x2e_009018_bit16 -F_0x2e_009018_bit17 -F_0x2e_009018_bit18 -F_0x2e_009018_bit19 -F_0x2e_018019_bit_10 -F_0x2e_018019_bit_9 -F_0x2e_018019_bit_8 -F_0x2e_018019_bit_7 -F_0x2e_018019_bit_6 -F_0x2e_018019_bit_5 -F_0x2e_018019_bit_4 -F_0x2e_018019_bit_3 -F_0x2e_018019_bit_2 -F_0x2e_018019_bit_1 -F_0x2e_018019_bit0 -F_0x2e_018019_bit1 -F_0x2e_018019_bit2 -F_0x2e_018019_bit3 -F_0x2e_018019_bit4 -F_0x2e_018019_bit5 -F_0x2e_018019_bit6 -F_0x2e_018019_bit7 -F_0x2e_018019_bit8 -F_0x2e_018019_bit9 -F_0x2e_018019_bit10 -F_0x2e_018019_bit11 -F_0x2e_018019_bit12 -F_0x2e_018019_bit13 -F_0x2e_018019_bit14 -F_0x2e_018019_bit15 -F_0x2e_018019_bit16 -F_0x2e_018019_bit17 -F_0x2e_018019_bit18 -F_0x2e_018019_bit19 -F_0x2e_019024_bit_10 -F_0x2e_019024_bit_9 -F_0x2e_019024_bit_8 -F_0x2e_019024_bit_7 -F_0x2e_019024_bit_6 -F_0x2e_019024_bit_5 -F_0x2e_019024_bit_4 -F_0x2e_019024_bit_3 -F_0x2e_019024_bit_2 -F_0x2e_019024_bit_1 -F_0x2e_019024_bit0 F_0x2e_019024_bit1 -F_0x2e_019024_bit2 -F_0x2e_019024_bit3 -F_0x2e_019024_bit4 -F_0x2e_019024_bit5 -F_0x2e_019024_bit6 -F_0x2e_019024_bit7 -F_0x2e_019024_bit8 -F_0x2e_019024_bit9 -F_0x2e_019024_bit10 -F_0x2e_019024_bit11 -F_0x2e_019024_bit12 -F_0x2e_019024_bit13 -F_0x2e_019024_bit14 -F_0x2e_019024_bit15 -F_0x2e_019024_bit16 -F_0x2e_019024_bit17 -F_0x2e_019024_bit18 -F_0x2e_019024_bit19 -F_0x2e_024_0x2e__0x2e__0x2e__bit_10 -F_0x2e_024_0x2e__0x2e__0x2e__bit_9 -F_0x2e_024_0x2e__0x2e__0x2e__bit_8 -F_0x2e_024_0x2e__0x2e__0x2e__bit_7 -F_0x2e_024_0x2e__0x2e__0x2e__bit_6 -F_0x2e_024_0x2e__0x2e__0x2e__bit_5 -F_0x2e_024_0x2e__0x2e__0x2e__bit_4 -F_0x2e_024_0x2e__0x2e__0x2e__bit_3 -F_0x2e_024_0x2e__0x2e__0x2e__bit_2 -F_0x2e_024_0x2e__0x2e__0x2e__bit_1 -F_0x2e_024_0x2e__0x2e__0x2e__bit0 -F_0x2e_024_0x2e__0x2e__0x2e__bit1 -F_0x2e_024_0x2e__0x2e__0x2e__bit2 -F_0x2e_024_0x2e__0x2e__0x2e__bit3 -F_0x2e_024_0x2e__0x2e__0x2e__bit4 -F_0x2e_024_0x2e__0x2e__0x2e__bit5 -F_0x2e_024_0x2e__0x2e__0x2e__bit6 -F_0x2e_024_0x2e__0x2e__0x2e__bit7 -F_0x2e_024_0x2e__0x2e__0x2e__bit8 -F_0x2e_024_0x2e__0x2e__0x2e__bit9 -F_0x2e_024_0x2e__0x2e__0x2e__bit10 -F_0x2e_024_0x2e__0x2e__0x2e__bit11 -F_0x2e_024_0x2e__0x2e__0x2e__bit12 -F_0x2e_024_0x2e__0x2e__0x2e__bit13 -F_0x2e_024_0x2e__0x2e__0x2e__bit14 -F_0x2e_024_0x2e__0x2e__0x2e__bit15 -F_0x2e_024_0x2e__0x2e__0x2e__bit16 -F_0x2e_024_0x2e__0x2e__0x2e__bit17 -F_0x2e_024_0x2e__0x2e__0x2e__bit18 -F_0x2e_024_0x2e__0x2e__0x2e__bit19 -F_0x2e_023024_bit_10 -F_0x2e_023024_bit_9 -F_0x2e_023024_bit_8 -F_0x2e_023024_bit_7 -F_0x2e_023024_bit_6 -F_0x2e_023024_bit_5 -F_0x2e_023024_bit_4 -F_0x2e_023024_bit_3 -F_0x2e_023024_bit_2 -F_0x2e_023024_bit_1 -F_0x2e_023024_bit0 -F_0x2e_023024_bit1 -F_0x2e_023024_bit2 -F_0x2e_023024_bit3 -F_0x2e_023024_bit4 -F_0x2e_023024_bit5 -F_0x2e_023024_bit6 -F_0x2e_023024_bit7 -F_0x2e_023024_bit8 -F_0x2e_023024_bit9 -F_0x2e_023024_bit10 -F_0x2e_023024_bit11 -F_0x2e_023024_bit12 -F_0x2e_023024_bit13 -F_0x2e_023024_bit14 -F_0x2e_023024_bit15 -F_0x2e_023024_bit16 -F_0x2e_023024_bit17 -F_0x2e_023024_bit18 -F_0x2e_023024_bit19 -F_0x2e_022023_bit_10 -F_0x2e_022023_bit_9 -F_0x2e_022023_bit_8 -F_0x2e_022023_bit_7 -F_0x2e_022023_bit_6 -F_0x2e_022023_bit_5 -F_0x2e_022023_bit_4 -F_0x2e_022023_bit_3 -F_0x2e_022023_bit_2 -F_0x2e_022023_bit_1 -F_0x2e_022023_bit0 -F_0x2e_022023_bit1 -F_0x2e_022023_bit2 -F_0x2e_022023_bit3 -F_0x2e_022023_bit4 -F_0x2e_022023_bit5 -F_0x2e_022023_bit6 -F_0x2e_022023_bit7 -F_0x2e_022023_bit8 -F_0x2e_022023_bit9 -F_0x2e_022023_bit10 -F_0x2e_022023_bit11 -F_0x2e_022023_bit12 -F_0x2e_022023_bit13 -F_0x2e_022023_bit14 -F_0x2e_022023_bit15 -F_0x2e_022023_bit16 -F_0x2e_022023_bit17 -F_0x2e_022023_bit18 -F_0x2e_022023_bit19 -F_0x2e_020022_bit_10 -F_0x2e_020022_bit_9 -F_0x2e_020022_bit_8 -F_0x2e_020022_bit_7 -F_0x2e_020022_bit_6 -F_0x2e_020022_bit_5 -F_0x2e_020022_bit_4 -F_0x2e_020022_bit_3 -F_0x2e_020022_bit_2 -F_0x2e_020022_bit_1 -F_0x2e_020022_bit0 -F_0x2e_020022_bit1 -F_0x2e_020022_bit2 -F_0x2e_020022_bit3 -F_0x2e_020022_bit4 -F_0x2e_020022_bit5 -F_0x2e_020022_bit6 -F_0x2e_020022_bit7 -F_0x2e_020022_bit8 -F_0x2e_020022_bit9 -F_0x2e_020022_bit10 -F_0x2e_020022_bit11 -F_0x2e_020022_bit12 -F_0x2e_020022_bit13 -F_0x2e_020022_bit14 -F_0x2e_020022_bit15 -F_0x2e_020022_bit16 -F_0x2e_020022_bit17 -F_0x2e_020022_bit18 -F_0x2e_020022_bit19 -F_0x2e_021022_bit_10 -F_0x2e_021022_bit_9 -F_0x2e_021022_bit_8 -F_0x2e_021022_bit_7 -F_0x2e_021022_bit_6 -F_0x2e_021022_bit_5 -F_0x2e_021022_bit_4 -F_0x2e_021022_bit_3 -F_0x2e_021022_bit_2 -F_0x2e_021022_bit_1 F_0x2e_021022_bit0 F_0x2e_021022_bit1 F_0x2e_021022_bit2 -F_0x2e_021022_bit3 -F_0x2e_021022_bit4 -F_0x2e_021022_bit5 -F_0x2e_021022_bit6 -F_0x2e_021022_bit7 -F_0x2e_021022_bit8 -F_0x2e_021022_bit9 -F_0x2e_021022_bit10 -F_0x2e_021022_bit11 -F_0x2e_021022_bit12 -F_0x2e_021022_bit13 -F_0x2e_021022_bit14 -F_0x2e_021022_bit15 -F_0x2e_021022_bit16 -F_0x2e_021022_bit17 -F_0x2e_021022_bit18 -F_0x2e_021022_bit19 -F_0x2e_022_0x2e__0x2e__0x2e__bit_10 -F_0x2e_022_0x2e__0x2e__0x2e__bit_9 -F_0x2e_022_0x2e__0x2e__0x2e__bit_8 -F_0x2e_022_0x2e__0x2e__0x2e__bit_7 -F_0x2e_022_0x2e__0x2e__0x2e__bit_6 -F_0x2e_022_0x2e__0x2e__0x2e__bit_5 -F_0x2e_022_0x2e__0x2e__0x2e__bit_4 -F_0x2e_022_0x2e__0x2e__0x2e__bit_3 -F_0x2e_022_0x2e__0x2e__0x2e__bit_2 -F_0x2e_022_0x2e__0x2e__0x2e__bit_1 F_0x2e_022_0x2e__0x2e__0x2e__bit0 F_0x2e_022_0x2e__0x2e__0x2e__bit1 F_0x2e_022_0x2e__0x2e__0x2e__bit2 -F_0x2e_022_0x2e__0x2e__0x2e__bit3 -F_0x2e_022_0x2e__0x2e__0x2e__bit4 -F_0x2e_022_0x2e__0x2e__0x2e__bit5 -F_0x2e_022_0x2e__0x2e__0x2e__bit6 -F_0x2e_022_0x2e__0x2e__0x2e__bit7 -F_0x2e_022_0x2e__0x2e__0x2e__bit8 -F_0x2e_022_0x2e__0x2e__0x2e__bit9 -F_0x2e_022_0x2e__0x2e__0x2e__bit10 -F_0x2e_022_0x2e__0x2e__0x2e__bit11 -F_0x2e_022_0x2e__0x2e__0x2e__bit12 -F_0x2e_022_0x2e__0x2e__0x2e__bit13 -F_0x2e_022_0x2e__0x2e__0x2e__bit14 -F_0x2e_022_0x2e__0x2e__0x2e__bit15 -F_0x2e_022_0x2e__0x2e__0x2e__bit16 -F_0x2e_022_0x2e__0x2e__0x2e__bit17 -F_0x2e_022_0x2e__0x2e__0x2e__bit18 -F_0x2e_022_0x2e__0x2e__0x2e__bit19 -F_0x2e_024026_bit_10 -F_0x2e_024026_bit_9 -F_0x2e_024026_bit_8 -F_0x2e_024026_bit_7 -F_0x2e_024026_bit_6 -F_0x2e_024026_bit_5 -F_0x2e_024026_bit_4 -F_0x2e_024026_bit_3 -F_0x2e_024026_bit_2 -F_0x2e_024026_bit_1 -F_0x2e_024026_bit0 F_0x2e_024026_bit1 -F_0x2e_024026_bit2 -F_0x2e_024026_bit3 -F_0x2e_024026_bit4 -F_0x2e_024026_bit5 -F_0x2e_024026_bit6 -F_0x2e_024026_bit7 -F_0x2e_024026_bit8 -F_0x2e_024026_bit9 -F_0x2e_024026_bit10 -F_0x2e_024026_bit11 -F_0x2e_024026_bit12 -F_0x2e_024026_bit13 -F_0x2e_024026_bit14 -F_0x2e_024026_bit15 -F_0x2e_024026_bit16 -F_0x2e_024026_bit17 -F_0x2e_024026_bit18 -F_0x2e_024026_bit19 -F_0x2e_025026_bit_10 -F_0x2e_025026_bit_9 -F_0x2e_025026_bit_8 -F_0x2e_025026_bit_7 -F_0x2e_025026_bit_6 -F_0x2e_025026_bit_5 -F_0x2e_025026_bit_4 -F_0x2e_025026_bit_3 -F_0x2e_025026_bit_2 -F_0x2e_025026_bit_1 F_0x2e_025026_bit0 F_0x2e_025026_bit1 -F_0x2e_025026_bit2 -F_0x2e_025026_bit3 F_0x2e_025026_bit4 -F_0x2e_025026_bit5 -F_0x2e_025026_bit6 -F_0x2e_025026_bit7 -F_0x2e_025026_bit8 -F_0x2e_025026_bit9 -F_0x2e_025026_bit10 -F_0x2e_025026_bit11 -F_0x2e_025026_bit12 -F_0x2e_025026_bit13 -F_0x2e_025026_bit14 -F_0x2e_025026_bit15 -F_0x2e_025026_bit16 -F_0x2e_025026_bit17 -F_0x2e_025026_bit18 -F_0x2e_025026_bit19 -F_0x2e_025_0x2e__0x2e__0x2e__bit_10 -F_0x2e_025_0x2e__0x2e__0x2e__bit_9 -F_0x2e_025_0x2e__0x2e__0x2e__bit_8 -F_0x2e_025_0x2e__0x2e__0x2e__bit_7 -F_0x2e_025_0x2e__0x2e__0x2e__bit_6 -F_0x2e_025_0x2e__0x2e__0x2e__bit_5 -F_0x2e_025_0x2e__0x2e__0x2e__bit_4 -F_0x2e_025_0x2e__0x2e__0x2e__bit_3 -F_0x2e_025_0x2e__0x2e__0x2e__bit_2 -F_0x2e_025_0x2e__0x2e__0x2e__bit_1 -F_0x2e_025_0x2e__0x2e__0x2e__bit0 -F_0x2e_025_0x2e__0x2e__0x2e__bit1 -F_0x2e_025_0x2e__0x2e__0x2e__bit2 -F_0x2e_025_0x2e__0x2e__0x2e__bit3 -F_0x2e_025_0x2e__0x2e__0x2e__bit4 -F_0x2e_025_0x2e__0x2e__0x2e__bit5 -F_0x2e_025_0x2e__0x2e__0x2e__bit6 -F_0x2e_025_0x2e__0x2e__0x2e__bit7 -F_0x2e_025_0x2e__0x2e__0x2e__bit8 -F_0x2e_025_0x2e__0x2e__0x2e__bit9 -F_0x2e_025_0x2e__0x2e__0x2e__bit10 -F_0x2e_025_0x2e__0x2e__0x2e__bit11 -F_0x2e_025_0x2e__0x2e__0x2e__bit12 -F_0x2e_025_0x2e__0x2e__0x2e__bit13 -F_0x2e_025_0x2e__0x2e__0x2e__bit14 -F_0x2e_025_0x2e__0x2e__0x2e__bit15 -F_0x2e_025_0x2e__0x2e__0x2e__bit16 -F_0x2e_025_0x2e__0x2e__0x2e__bit17 -F_0x2e_025_0x2e__0x2e__0x2e__bit18 -F_0x2e_025_0x2e__0x2e__0x2e__bit19 -F_0x2e_026027_bit_10 -F_0x2e_026027_bit_9 -F_0x2e_026027_bit_8 -F_0x2e_026027_bit_7 -F_0x2e_026027_bit_6 -F_0x2e_026027_bit_5 -F_0x2e_026027_bit_4 -F_0x2e_026027_bit_3 -F_0x2e_026027_bit_2 -F_0x2e_026027_bit_1 F_0x2e_026027_bit0 F_0x2e_026027_bit1 F_0x2e_026027_bit2 F_0x2e_026027_bit3 F_0x2e_026027_bit4 -F_0x2e_026027_bit5 -F_0x2e_026027_bit6 -F_0x2e_026027_bit7 -F_0x2e_026027_bit8 -F_0x2e_026027_bit9 -F_0x2e_026027_bit10 -F_0x2e_026027_bit11 -F_0x2e_026027_bit12 -F_0x2e_026027_bit13 -F_0x2e_026027_bit14 -F_0x2e_026027_bit15 -F_0x2e_026027_bit16 -F_0x2e_026027_bit17 -F_0x2e_026027_bit18 -F_0x2e_026027_bit19 -F_0x2e_027_0x2e__0x2e__0x2e__bit_10 -F_0x2e_027_0x2e__0x2e__0x2e__bit_9 -F_0x2e_027_0x2e__0x2e__0x2e__bit_8 -F_0x2e_027_0x2e__0x2e__0x2e__bit_7 -F_0x2e_027_0x2e__0x2e__0x2e__bit_6 -F_0x2e_027_0x2e__0x2e__0x2e__bit_5 -F_0x2e_027_0x2e__0x2e__0x2e__bit_4 -F_0x2e_027_0x2e__0x2e__0x2e__bit_3 -F_0x2e_027_0x2e__0x2e__0x2e__bit_2 -F_0x2e_027_0x2e__0x2e__0x2e__bit_1 -F_0x2e_027_0x2e__0x2e__0x2e__bit0 -F_0x2e_027_0x2e__0x2e__0x2e__bit1 -F_0x2e_027_0x2e__0x2e__0x2e__bit2 -F_0x2e_027_0x2e__0x2e__0x2e__bit3 -F_0x2e_027_0x2e__0x2e__0x2e__bit4 -F_0x2e_027_0x2e__0x2e__0x2e__bit5 -F_0x2e_027_0x2e__0x2e__0x2e__bit6 -F_0x2e_027_0x2e__0x2e__0x2e__bit7 -F_0x2e_027_0x2e__0x2e__0x2e__bit8 -F_0x2e_027_0x2e__0x2e__0x2e__bit9 -F_0x2e_027_0x2e__0x2e__0x2e__bit10 -F_0x2e_027_0x2e__0x2e__0x2e__bit11 -F_0x2e_027_0x2e__0x2e__0x2e__bit12 -F_0x2e_027_0x2e__0x2e__0x2e__bit13 -F_0x2e_027_0x2e__0x2e__0x2e__bit14 -F_0x2e_027_0x2e__0x2e__0x2e__bit15 -F_0x2e_027_0x2e__0x2e__0x2e__bit16 -F_0x2e_027_0x2e__0x2e__0x2e__bit17 -F_0x2e_027_0x2e__0x2e__0x2e__bit18 -F_0x2e_027_0x2e__0x2e__0x2e__bit19 -F_0x2e_027032_bit_10 -F_0x2e_027032_bit_9 -F_0x2e_027032_bit_8 -F_0x2e_027032_bit_7 -F_0x2e_027032_bit_6 -F_0x2e_027032_bit_5 -F_0x2e_027032_bit_4 -F_0x2e_027032_bit_3 -F_0x2e_027032_bit_2 -F_0x2e_027032_bit_1 F_0x2e_027032_bit0 F_0x2e_027032_bit1 F_0x2e_027032_bit2 F_0x2e_027032_bit3 F_0x2e_027032_bit4 -F_0x2e_027032_bit5 -F_0x2e_027032_bit6 -F_0x2e_027032_bit7 -F_0x2e_027032_bit8 -F_0x2e_027032_bit9 -F_0x2e_027032_bit10 -F_0x2e_027032_bit11 -F_0x2e_027032_bit12 -F_0x2e_027032_bit13 -F_0x2e_027032_bit14 -F_0x2e_027032_bit15 -F_0x2e_027032_bit16 -F_0x2e_027032_bit17 -F_0x2e_027032_bit18 -F_0x2e_027032_bit19 -F_0x2e_030031_bit_10 -F_0x2e_030031_bit_9 -F_0x2e_030031_bit_8 -F_0x2e_030031_bit_7 -F_0x2e_030031_bit_6 -F_0x2e_030031_bit_5 -F_0x2e_030031_bit_4 -F_0x2e_030031_bit_3 -F_0x2e_030031_bit_2 -F_0x2e_030031_bit_1 -F_0x2e_030031_bit0 -F_0x2e_030031_bit1 -F_0x2e_030031_bit2 -F_0x2e_030031_bit3 -F_0x2e_030031_bit4 -F_0x2e_030031_bit5 -F_0x2e_030031_bit6 -F_0x2e_030031_bit7 -F_0x2e_030031_bit8 -F_0x2e_030031_bit9 -F_0x2e_030031_bit10 -F_0x2e_030031_bit11 -F_0x2e_030031_bit12 -F_0x2e_030031_bit13 -F_0x2e_030031_bit14 -F_0x2e_030031_bit15 -F_0x2e_030031_bit16 -F_0x2e_030031_bit17 -F_0x2e_030031_bit18 -F_0x2e_030031_bit19 -F_0x2e_031032_bit_10 -F_0x2e_031032_bit_9 -F_0x2e_031032_bit_8 -F_0x2e_031032_bit_7 -F_0x2e_031032_bit_6 -F_0x2e_031032_bit_5 -F_0x2e_031032_bit_4 -F_0x2e_031032_bit_3 -F_0x2e_031032_bit_2 -F_0x2e_031032_bit_1 F_0x2e_031032_bit0 -F_0x2e_031032_bit1 F_0x2e_031032_bit2 -F_0x2e_031032_bit3 -F_0x2e_031032_bit4 -F_0x2e_031032_bit5 -F_0x2e_031032_bit6 -F_0x2e_031032_bit7 -F_0x2e_031032_bit8 -F_0x2e_031032_bit9 -F_0x2e_031032_bit10 -F_0x2e_031032_bit11 -F_0x2e_031032_bit12 -F_0x2e_031032_bit13 -F_0x2e_031032_bit14 -F_0x2e_031032_bit15 -F_0x2e_031032_bit16 -F_0x2e_031032_bit17 -F_0x2e_031032_bit18 -F_0x2e_031032_bit19 -F_0x2e_029031_bit_10 -F_0x2e_029031_bit_9 -F_0x2e_029031_bit_8 -F_0x2e_029031_bit_7 -F_0x2e_029031_bit_6 -F_0x2e_029031_bit_5 -F_0x2e_029031_bit_4 -F_0x2e_029031_bit_3 -F_0x2e_029031_bit_2 -F_0x2e_029031_bit_1 F_0x2e_029031_bit0 -F_0x2e_029031_bit1 F_0x2e_029031_bit2 -F_0x2e_029031_bit3 -F_0x2e_029031_bit4 -F_0x2e_029031_bit5 -F_0x2e_029031_bit6 -F_0x2e_029031_bit7 -F_0x2e_029031_bit8 -F_0x2e_029031_bit9 -F_0x2e_029031_bit10 -F_0x2e_029031_bit11 -F_0x2e_029031_bit12 -F_0x2e_029031_bit13 -F_0x2e_029031_bit14 -F_0x2e_029031_bit15 -F_0x2e_029031_bit16 -F_0x2e_029031_bit17 -F_0x2e_029031_bit18 -F_0x2e_029031_bit19 -F_0x2e_028029_bit_10 -F_0x2e_028029_bit_9 -F_0x2e_028029_bit_8 -F_0x2e_028029_bit_7 -F_0x2e_028029_bit_6 -F_0x2e_028029_bit_5 -F_0x2e_028029_bit_4 -F_0x2e_028029_bit_3 -F_0x2e_028029_bit_2 -F_0x2e_028029_bit_1 -F_0x2e_028029_bit0 -F_0x2e_028029_bit1 -F_0x2e_028029_bit2 -F_0x2e_028029_bit3 -F_0x2e_028029_bit4 -F_0x2e_028029_bit5 -F_0x2e_028029_bit6 -F_0x2e_028029_bit7 -F_0x2e_028029_bit8 -F_0x2e_028029_bit9 -F_0x2e_028029_bit10 -F_0x2e_028029_bit11 -F_0x2e_028029_bit12 -F_0x2e_028029_bit13 -F_0x2e_028029_bit14 -F_0x2e_028029_bit15 -F_0x2e_028029_bit16 -F_0x2e_028029_bit17 -F_0x2e_028029_bit18 -F_0x2e_028029_bit19 -F_0x2e_028_0x2e__0x2e__0x2e__bit_10 -F_0x2e_028_0x2e__0x2e__0x2e__bit_9 -F_0x2e_028_0x2e__0x2e__0x2e__bit_8 -F_0x2e_028_0x2e__0x2e__0x2e__bit_7 -F_0x2e_028_0x2e__0x2e__0x2e__bit_6 -F_0x2e_028_0x2e__0x2e__0x2e__bit_5 -F_0x2e_028_0x2e__0x2e__0x2e__bit_4 -F_0x2e_028_0x2e__0x2e__0x2e__bit_3 -F_0x2e_028_0x2e__0x2e__0x2e__bit_2 -F_0x2e_028_0x2e__0x2e__0x2e__bit_1 -F_0x2e_028_0x2e__0x2e__0x2e__bit0 -F_0x2e_028_0x2e__0x2e__0x2e__bit1 -F_0x2e_028_0x2e__0x2e__0x2e__bit2 -F_0x2e_028_0x2e__0x2e__0x2e__bit3 -F_0x2e_028_0x2e__0x2e__0x2e__bit4 -F_0x2e_028_0x2e__0x2e__0x2e__bit5 -F_0x2e_028_0x2e__0x2e__0x2e__bit6 -F_0x2e_028_0x2e__0x2e__0x2e__bit7 -F_0x2e_028_0x2e__0x2e__0x2e__bit8 -F_0x2e_028_0x2e__0x2e__0x2e__bit9 -F_0x2e_028_0x2e__0x2e__0x2e__bit10 -F_0x2e_028_0x2e__0x2e__0x2e__bit11 -F_0x2e_028_0x2e__0x2e__0x2e__bit12 -F_0x2e_028_0x2e__0x2e__0x2e__bit13 -F_0x2e_028_0x2e__0x2e__0x2e__bit14 -F_0x2e_028_0x2e__0x2e__0x2e__bit15 -F_0x2e_028_0x2e__0x2e__0x2e__bit16 -F_0x2e_028_0x2e__0x2e__0x2e__bit17 -F_0x2e_028_0x2e__0x2e__0x2e__bit18 -F_0x2e_028_0x2e__0x2e__0x2e__bit19 -F_0x2e_032033_bit_10 -F_0x2e_032033_bit_9 -F_0x2e_032033_bit_8 -F_0x2e_032033_bit_7 -F_0x2e_032033_bit_6 -F_0x2e_032033_bit_5 -F_0x2e_032033_bit_4 -F_0x2e_032033_bit_3 -F_0x2e_032033_bit_2 -F_0x2e_032033_bit_1 -F_0x2e_032033_bit0 -F_0x2e_032033_bit1 F_0x2e_032033_bit2 -F_0x2e_032033_bit3 -F_0x2e_032033_bit4 F_0x2e_032033_bit5 -F_0x2e_032033_bit6 -F_0x2e_032033_bit7 -F_0x2e_032033_bit8 -F_0x2e_032033_bit9 -F_0x2e_032033_bit10 -F_0x2e_032033_bit11 -F_0x2e_032033_bit12 -F_0x2e_032033_bit13 -F_0x2e_032033_bit14 -F_0x2e_032033_bit15 -F_0x2e_032033_bit16 -F_0x2e_032033_bit17 -F_0x2e_032033_bit18 -F_0x2e_032033_bit19 -F_0x2e_033037_bit_10 -F_0x2e_033037_bit_9 -F_0x2e_033037_bit_8 -F_0x2e_033037_bit_7 -F_0x2e_033037_bit_6 -F_0x2e_033037_bit_5 -F_0x2e_033037_bit_4 -F_0x2e_033037_bit_3 -F_0x2e_033037_bit_2 -F_0x2e_033037_bit_1 -F_0x2e_033037_bit0 -F_0x2e_033037_bit1 F_0x2e_033037_bit2 -F_0x2e_033037_bit3 -F_0x2e_033037_bit4 F_0x2e_033037_bit5 -F_0x2e_033037_bit6 -F_0x2e_033037_bit7 -F_0x2e_033037_bit8 -F_0x2e_033037_bit9 -F_0x2e_033037_bit10 -F_0x2e_033037_bit11 -F_0x2e_033037_bit12 -F_0x2e_033037_bit13 -F_0x2e_033037_bit14 -F_0x2e_033037_bit15 -F_0x2e_033037_bit16 -F_0x2e_033037_bit17 -F_0x2e_033037_bit18 -F_0x2e_033037_bit19 -F_0x2e_034036_bit_10 -F_0x2e_034036_bit_9 -F_0x2e_034036_bit_8 -F_0x2e_034036_bit_7 -F_0x2e_034036_bit_6 -F_0x2e_034036_bit_5 -F_0x2e_034036_bit_4 -F_0x2e_034036_bit_3 -F_0x2e_034036_bit_2 -F_0x2e_034036_bit_1 -F_0x2e_034036_bit0 -F_0x2e_034036_bit1 -F_0x2e_034036_bit2 -F_0x2e_034036_bit3 -F_0x2e_034036_bit4 -F_0x2e_034036_bit5 -F_0x2e_034036_bit6 -F_0x2e_034036_bit7 -F_0x2e_034036_bit8 -F_0x2e_034036_bit9 -F_0x2e_034036_bit10 -F_0x2e_034036_bit11 -F_0x2e_034036_bit12 -F_0x2e_034036_bit13 -F_0x2e_034036_bit14 -F_0x2e_034036_bit15 -F_0x2e_034036_bit16 -F_0x2e_034036_bit17 -F_0x2e_034036_bit18 -F_0x2e_034036_bit19 -F_0x2e_035036_bit_10 -F_0x2e_035036_bit_9 -F_0x2e_035036_bit_8 -F_0x2e_035036_bit_7 -F_0x2e_035036_bit_6 -F_0x2e_035036_bit_5 -F_0x2e_035036_bit_4 -F_0x2e_035036_bit_3 -F_0x2e_035036_bit_2 -F_0x2e_035036_bit_1 -F_0x2e_035036_bit0 -F_0x2e_035036_bit1 -F_0x2e_035036_bit2 -F_0x2e_035036_bit3 -F_0x2e_035036_bit4 -F_0x2e_035036_bit5 -F_0x2e_035036_bit6 -F_0x2e_035036_bit7 -F_0x2e_035036_bit8 -F_0x2e_035036_bit9 -F_0x2e_035036_bit10 -F_0x2e_035036_bit11 -F_0x2e_035036_bit12 -F_0x2e_035036_bit13 -F_0x2e_035036_bit14 -F_0x2e_035036_bit15 -F_0x2e_035036_bit16 -F_0x2e_035036_bit17 -F_0x2e_035036_bit18 -F_0x2e_035036_bit19 -F_0x2e_037038_bit_10 -F_0x2e_037038_bit_9 -F_0x2e_037038_bit_8 -F_0x2e_037038_bit_7 -F_0x2e_037038_bit_6 -F_0x2e_037038_bit_5 -F_0x2e_037038_bit_4 -F_0x2e_037038_bit_3 -F_0x2e_037038_bit_2 -F_0x2e_037038_bit_1 -F_0x2e_037038_bit0 -F_0x2e_037038_bit1 F_0x2e_037038_bit2 -F_0x2e_037038_bit3 -F_0x2e_037038_bit4 F_0x2e_037038_bit5 -F_0x2e_037038_bit6 -F_0x2e_037038_bit7 -F_0x2e_037038_bit8 -F_0x2e_037038_bit9 -F_0x2e_037038_bit10 -F_0x2e_037038_bit11 -F_0x2e_037038_bit12 -F_0x2e_037038_bit13 -F_0x2e_037038_bit14 -F_0x2e_037038_bit15 -F_0x2e_037038_bit16 -F_0x2e_037038_bit17 -F_0x2e_037038_bit18 -F_0x2e_037038_bit19 -F_0x2e_039040_bit_10 -F_0x2e_039040_bit_9 -F_0x2e_039040_bit_8 -F_0x2e_039040_bit_7 -F_0x2e_039040_bit_6 -F_0x2e_039040_bit_5 -F_0x2e_039040_bit_4 -F_0x2e_039040_bit_3 -F_0x2e_039040_bit_2 -F_0x2e_039040_bit_1 F_0x2e_039040_bit0 -F_0x2e_039040_bit1 F_0x2e_039040_bit2 -F_0x2e_039040_bit3 -F_0x2e_039040_bit4 -F_0x2e_039040_bit5 -F_0x2e_039040_bit6 -F_0x2e_039040_bit7 -F_0x2e_039040_bit8 -F_0x2e_039040_bit9 -F_0x2e_039040_bit10 -F_0x2e_039040_bit11 -F_0x2e_039040_bit12 -F_0x2e_039040_bit13 -F_0x2e_039040_bit14 -F_0x2e_039040_bit15 -F_0x2e_039040_bit16 -F_0x2e_039040_bit17 -F_0x2e_039040_bit18 -F_0x2e_039040_bit19 -F_0x2e_040_0x2e__0x2e__0x2e__bit_10 -F_0x2e_040_0x2e__0x2e__0x2e__bit_9 -F_0x2e_040_0x2e__0x2e__0x2e__bit_8 -F_0x2e_040_0x2e__0x2e__0x2e__bit_7 -F_0x2e_040_0x2e__0x2e__0x2e__bit_6 -F_0x2e_040_0x2e__0x2e__0x2e__bit_5 -F_0x2e_040_0x2e__0x2e__0x2e__bit_4 -F_0x2e_040_0x2e__0x2e__0x2e__bit_3 -F_0x2e_040_0x2e__0x2e__0x2e__bit_2 -F_0x2e_040_0x2e__0x2e__0x2e__bit_1 -F_0x2e_040_0x2e__0x2e__0x2e__bit0 -F_0x2e_040_0x2e__0x2e__0x2e__bit1 -F_0x2e_040_0x2e__0x2e__0x2e__bit2 -F_0x2e_040_0x2e__0x2e__0x2e__bit3 -F_0x2e_040_0x2e__0x2e__0x2e__bit4 -F_0x2e_040_0x2e__0x2e__0x2e__bit5 -F_0x2e_040_0x2e__0x2e__0x2e__bit6 -F_0x2e_040_0x2e__0x2e__0x2e__bit7 -F_0x2e_040_0x2e__0x2e__0x2e__bit8 -F_0x2e_040_0x2e__0x2e__0x2e__bit9 -F_0x2e_040_0x2e__0x2e__0x2e__bit10 -F_0x2e_040_0x2e__0x2e__0x2e__bit11 -F_0x2e_040_0x2e__0x2e__0x2e__bit12 -F_0x2e_040_0x2e__0x2e__0x2e__bit13 -F_0x2e_040_0x2e__0x2e__0x2e__bit14 -F_0x2e_040_0x2e__0x2e__0x2e__bit15 -F_0x2e_040_0x2e__0x2e__0x2e__bit16 -F_0x2e_040_0x2e__0x2e__0x2e__bit17 -F_0x2e_040_0x2e__0x2e__0x2e__bit18 -F_0x2e_040_0x2e__0x2e__0x2e__bit19 -F_0x2e_041_0x2e__0x2e__0x2e__bit_10 -F_0x2e_041_0x2e__0x2e__0x2e__bit_9 -F_0x2e_041_0x2e__0x2e__0x2e__bit_8 -F_0x2e_041_0x2e__0x2e__0x2e__bit_7 -F_0x2e_041_0x2e__0x2e__0x2e__bit_6 -F_0x2e_041_0x2e__0x2e__0x2e__bit_5 -F_0x2e_041_0x2e__0x2e__0x2e__bit_4 -F_0x2e_041_0x2e__0x2e__0x2e__bit_3 -F_0x2e_041_0x2e__0x2e__0x2e__bit_2 -F_0x2e_041_0x2e__0x2e__0x2e__bit_1 -F_0x2e_041_0x2e__0x2e__0x2e__bit0 -F_0x2e_041_0x2e__0x2e__0x2e__bit1 -F_0x2e_041_0x2e__0x2e__0x2e__bit2 -F_0x2e_041_0x2e__0x2e__0x2e__bit3 -F_0x2e_041_0x2e__0x2e__0x2e__bit4 -F_0x2e_041_0x2e__0x2e__0x2e__bit5 -F_0x2e_041_0x2e__0x2e__0x2e__bit6 -F_0x2e_041_0x2e__0x2e__0x2e__bit7 -F_0x2e_041_0x2e__0x2e__0x2e__bit8 -F_0x2e_041_0x2e__0x2e__0x2e__bit9 -F_0x2e_041_0x2e__0x2e__0x2e__bit10 -F_0x2e_041_0x2e__0x2e__0x2e__bit11 -F_0x2e_041_0x2e__0x2e__0x2e__bit12 -F_0x2e_041_0x2e__0x2e__0x2e__bit13 -F_0x2e_041_0x2e__0x2e__0x2e__bit14 -F_0x2e_041_0x2e__0x2e__0x2e__bit15 -F_0x2e_041_0x2e__0x2e__0x2e__bit16 -F_0x2e_041_0x2e__0x2e__0x2e__bit17 -F_0x2e_041_0x2e__0x2e__0x2e__bit18 -F_0x2e_041_0x2e__0x2e__0x2e__bit19 -F_0x2e_040041_bit_10 -F_0x2e_040041_bit_9 -F_0x2e_040041_bit_8 -F_0x2e_040041_bit_7 -F_0x2e_040041_bit_6 -F_0x2e_040041_bit_5 -F_0x2e_040041_bit_4 -F_0x2e_040041_bit_3 -F_0x2e_040041_bit_2 -F_0x2e_040041_bit_1 -F_0x2e_040041_bit0 F_0x2e_040041_bit1 F_0x2e_040041_bit2 F_0x2e_040041_bit3 -F_0x2e_040041_bit4 F_0x2e_040041_bit5 -F_0x2e_040041_bit6 -F_0x2e_040041_bit7 -F_0x2e_040041_bit8 -F_0x2e_040041_bit9 -F_0x2e_040041_bit10 -F_0x2e_040041_bit11 -F_0x2e_040041_bit12 -F_0x2e_040041_bit13 -F_0x2e_040041_bit14 -F_0x2e_040041_bit15 -F_0x2e_040041_bit16 -F_0x2e_040041_bit17 -F_0x2e_040041_bit18 -F_0x2e_040041_bit19 -F_0x2e_041042_bit_10 -F_0x2e_041042_bit_9 -F_0x2e_041042_bit_8 -F_0x2e_041042_bit_7 -F_0x2e_041042_bit_6 -F_0x2e_041042_bit_5 -F_0x2e_041042_bit_4 -F_0x2e_041042_bit_3 -F_0x2e_041042_bit_2 -F_0x2e_041042_bit_1 F_0x2e_041042_bit0 F_0x2e_041042_bit1 -F_0x2e_041042_bit2 -F_0x2e_041042_bit3 F_0x2e_041042_bit4 F_0x2e_041042_bit5 -F_0x2e_041042_bit6 -F_0x2e_041042_bit7 -F_0x2e_041042_bit8 -F_0x2e_041042_bit9 -F_0x2e_041042_bit10 -F_0x2e_041042_bit11 -F_0x2e_041042_bit12 -F_0x2e_041042_bit13 -F_0x2e_041042_bit14 -F_0x2e_041042_bit15 -F_0x2e_041042_bit16 -F_0x2e_041042_bit17 -F_0x2e_041042_bit18 -F_0x2e_041042_bit19 -F_0x2e_042_0x2e__0x2e__0x2e__bit_10 -F_0x2e_042_0x2e__0x2e__0x2e__bit_9 -F_0x2e_042_0x2e__0x2e__0x2e__bit_8 -F_0x2e_042_0x2e__0x2e__0x2e__bit_7 -F_0x2e_042_0x2e__0x2e__0x2e__bit_6 -F_0x2e_042_0x2e__0x2e__0x2e__bit_5 -F_0x2e_042_0x2e__0x2e__0x2e__bit_4 -F_0x2e_042_0x2e__0x2e__0x2e__bit_3 -F_0x2e_042_0x2e__0x2e__0x2e__bit_2 -F_0x2e_042_0x2e__0x2e__0x2e__bit_1 F_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_042_0x2e__0x2e__0x2e__bit1 -F_0x2e_042_0x2e__0x2e__0x2e__bit2 F_0x2e_042_0x2e__0x2e__0x2e__bit3 F_0x2e_042_0x2e__0x2e__0x2e__bit4 F_0x2e_042_0x2e__0x2e__0x2e__bit5 -F_0x2e_042_0x2e__0x2e__0x2e__bit6 -F_0x2e_042_0x2e__0x2e__0x2e__bit7 -F_0x2e_042_0x2e__0x2e__0x2e__bit8 -F_0x2e_042_0x2e__0x2e__0x2e__bit9 -F_0x2e_042_0x2e__0x2e__0x2e__bit10 -F_0x2e_042_0x2e__0x2e__0x2e__bit11 -F_0x2e_042_0x2e__0x2e__0x2e__bit12 -F_0x2e_042_0x2e__0x2e__0x2e__bit13 -F_0x2e_042_0x2e__0x2e__0x2e__bit14 -F_0x2e_042_0x2e__0x2e__0x2e__bit15 -F_0x2e_042_0x2e__0x2e__0x2e__bit16 -F_0x2e_042_0x2e__0x2e__0x2e__bit17 -F_0x2e_042_0x2e__0x2e__0x2e__bit18 -F_0x2e_042_0x2e__0x2e__0x2e__bit19 -F_0x2e_011012_bit_10 -F_0x2e_011012_bit_9 -F_0x2e_011012_bit_8 -F_0x2e_011012_bit_7 -F_0x2e_011012_bit_6 -F_0x2e_011012_bit_5 -F_0x2e_011012_bit_4 -F_0x2e_011012_bit_3 -F_0x2e_011012_bit_2 -F_0x2e_011012_bit_1 F_0x2e_011012_bit0 -F_0x2e_011012_bit1 F_0x2e_011012_bit2 -F_0x2e_011012_bit3 F_0x2e_011012_bit4 -F_0x2e_011012_bit5 -F_0x2e_011012_bit6 -F_0x2e_011012_bit7 -F_0x2e_011012_bit8 -F_0x2e_011012_bit9 -F_0x2e_011012_bit10 -F_0x2e_011012_bit11 -F_0x2e_011012_bit12 -F_0x2e_011012_bit13 -F_0x2e_011012_bit14 -F_0x2e_011012_bit15 -F_0x2e_011012_bit16 -F_0x2e_011012_bit17 -F_0x2e_011012_bit18 -F_0x2e_011012_bit19 -F_0x2e_036037_bit_10 -F_0x2e_036037_bit_9 -F_0x2e_036037_bit_8 -F_0x2e_036037_bit_7 -F_0x2e_036037_bit_6 -F_0x2e_036037_bit_5 -F_0x2e_036037_bit_4 -F_0x2e_036037_bit_3 -F_0x2e_036037_bit_2 -F_0x2e_036037_bit_1 -F_0x2e_036037_bit0 -F_0x2e_036037_bit1 -F_0x2e_036037_bit2 -F_0x2e_036037_bit3 -F_0x2e_036037_bit4 -F_0x2e_036037_bit5 -F_0x2e_036037_bit6 -F_0x2e_036037_bit7 -F_0x2e_036037_bit8 -F_0x2e_036037_bit9 -F_0x2e_036037_bit10 -F_0x2e_036037_bit11 -F_0x2e_036037_bit12 -F_0x2e_036037_bit13 -F_0x2e_036037_bit14 -F_0x2e_036037_bit15 -F_0x2e_036037_bit16 -F_0x2e_036037_bit17 -F_0x2e_036037_bit18 -F_0x2e_036037_bit19 -F_0x2e_038040_bit_10 -F_0x2e_038040_bit_9 -F_0x2e_038040_bit_8 -F_0x2e_038040_bit_7 -F_0x2e_038040_bit_6 -F_0x2e_038040_bit_5 -F_0x2e_038040_bit_4 -F_0x2e_038040_bit_3 -F_0x2e_038040_bit_2 -F_0x2e_038040_bit_1 F_0x2e_038040_bit0 -F_0x2e_038040_bit1 -F_0x2e_038040_bit2 F_0x2e_038040_bit3 -F_0x2e_038040_bit4 F_0x2e_038040_bit5 -F_0x2e_038040_bit6 -F_0x2e_038040_bit7 -F_0x2e_038040_bit8 -F_0x2e_038040_bit9 -F_0x2e_038040_bit10 -F_0x2e_038040_bit11 -F_0x2e_038040_bit12 -F_0x2e_038040_bit13 -F_0x2e_038040_bit14 -F_0x2e_038040_bit15 -F_0x2e_038040_bit16 -F_0x2e_038040_bit17 -F_0x2e_038040_bit18 -F_0x2e_038040_bit19 c _______________________________________________________________________________ c c restarts : 120 c conflicts : 35629 (32 /sec) c decisions : 135746 (122 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 1117.2 s c _______________________________________________________________________________
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/8913/stat): 8913 (minisat+_script) R 8912 8913 16528 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1846531049 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/8913/statm): 174 3 169 147 0 27 0 [pid=8913] 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=8914 New process pid=8915 New process pid=8916 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 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=8916) exited with status: 0 One traced child (pid=8915) exited with status: 0 One traced child (pid=8914) exited with status: 0 New process pid=8917 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-egout.opb [startup+10.0043 s] Raw data (loadavg): 0.54 0.84 0.70 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 9747 0 0 0 916 38 0 0 25 0 1 0 1846531055 41119744 9429 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 10039 9429 145 145 0 9894 0 [pid=8917] vsize: 40156 Current children cumulated CPU time (s) 9.55 Current children cumulated vsize (Kb) 42280 [startup+20.005 s] Raw data (loadavg): 0.61 0.84 0.70 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 9785 0 0 0 1914 39 0 0 25 0 1 0 1846531055 41209856 9467 4294967295 134512640 135094434 3221224432 3221223092 134553517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 10061 9467 145 145 0 9916 0 [pid=8917] vsize: 40244 Current children cumulated CPU time (s) 19.54 Current children cumulated vsize (Kb) 42368 [startup+30.0067 s] Raw data (loadavg): 0.67 0.85 0.71 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 10062 0 0 0 2913 40 0 0 25 0 1 0 1846531055 42332160 9744 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 10335 9744 145 145 0 10190 0 [pid=8917] vsize: 41340 Current children cumulated CPU time (s) 29.54 Current children cumulated vsize (Kb) 43464 [startup+40.0074 s] Raw data (loadavg): 0.72 0.85 0.71 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14513 0 0 0 3878 59 0 0 25 0 1 0 1846531055 65654784 13827 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 16029 13827 145 145 0 15884 0 [pid=8917] vsize: 64116 Current children cumulated CPU time (s) 39.38 Current children cumulated vsize (Kb) 66240 [startup+50.0081 s] Raw data (loadavg): 0.76 0.86 0.71 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14597 0 0 0 4877 59 0 0 25 0 1 0 1846531055 65925120 13911 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 16095 13911 145 145 0 15950 0 [pid=8917] vsize: 64380 Current children cumulated CPU time (s) 49.37 Current children cumulated vsize (Kb) 66504 [startup+60.0087 s] Raw data (loadavg): 0.80 0.86 0.72 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14657 0 0 0 5876 60 0 0 25 0 1 0 1846531055 66101248 13971 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 16138 13971 145 145 0 15993 0 [pid=8917] vsize: 64552 Current children cumulated CPU time (s) 59.37 Current children cumulated vsize (Kb) 66676 [startup+70.0094 s] Raw data (loadavg): 0.83 0.86 0.72 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14776 0 0 0 6874 61 0 0 25 0 1 0 1846531055 66580480 14090 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 16255 14090 145 145 0 16110 0 [pid=8917] vsize: 65020 Current children cumulated CPU time (s) 69.36 Current children cumulated vsize (Kb) 67144 [startup+80.0111 s] Raw data (loadavg): 0.85 0.87 0.72 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14992 0 0 0 7873 62 0 0 25 0 1 0 1846531055 67129344 14306 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8917/statm): 16389 14306 145 145 0 16244 0 [pid=8917] vsize: 65556 Current children cumulated CPU time (s) 79.36 Current children cumulated vsize (Kb) 67680 [startup+90.0118 s] Raw data (loadavg): 0.88 0.87 0.72 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 18998 0 0 0 8839 78 0 0 25 0 1 0 1846531055 80711680 18312 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 19705 18312 145 145 0 19560 0 [pid=8917] vsize: 78820 Current children cumulated CPU time (s) 89.18 Current children cumulated vsize (Kb) 80944 [startup+100.011 s] Raw data (loadavg): 0.89 0.88 0.73 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19004 0 0 0 9839 79 0 0 25 0 1 0 1846531055 80736256 18318 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 19711 18318 145 145 0 19566 0 [pid=8917] vsize: 78844 Current children cumulated CPU time (s) 99.19 Current children cumulated vsize (Kb) 80968 [startup+110.012 s] Raw data (loadavg): 0.91 0.88 0.73 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19010 0 0 0 10839 79 0 0 25 0 1 0 1846531055 80760832 18324 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 19717 18324 145 145 0 19572 0 [pid=8917] vsize: 78868 Current children cumulated CPU time (s) 109.19 Current children cumulated vsize (Kb) 80992 [startup+120.013 s] Raw data (loadavg): 0.92 0.88 0.73 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19032 0 0 0 11839 79 0 0 25 0 1 0 1846531055 80879616 18346 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 19746 18346 145 145 0 19601 0 [pid=8917] vsize: 78984 Current children cumulated CPU time (s) 119.19 Current children cumulated vsize (Kb) 81108 [startup+130.013 s] Raw data (loadavg): 0.93 0.89 0.73 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19078 0 0 0 12839 79 0 0 25 0 1 0 1846531055 81104896 18392 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 19801 18392 145 145 0 19656 0 [pid=8917] vsize: 79204 Current children cumulated CPU time (s) 129.19 Current children cumulated vsize (Kb) 81328 [startup+140.014 s] Raw data (loadavg): 0.94 0.89 0.74 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19303 0 0 0 13838 80 0 0 25 0 1 0 1846531055 82276352 18617 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20087 18617 145 145 0 19942 0 [pid=8917] vsize: 80348 Current children cumulated CPU time (s) 139.19 Current children cumulated vsize (Kb) 82472 [startup+150.015 s] Raw data (loadavg): 0.95 0.89 0.74 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19315 0 0 0 14838 80 0 0 25 0 1 0 1846531055 82317312 18629 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20097 18629 145 145 0 19952 0 [pid=8917] vsize: 80388 Current children cumulated CPU time (s) 149.19 Current children cumulated vsize (Kb) 82512 [startup+160.016 s] Raw data (loadavg): 0.96 0.90 0.74 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19331 0 0 0 15837 80 0 0 25 0 1 0 1846531055 82382848 18645 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20113 18645 145 145 0 19968 0 [pid=8917] vsize: 80452 Current children cumulated CPU time (s) 159.18 Current children cumulated vsize (Kb) 82576 [startup+170.016 s] Raw data (loadavg): 0.97 0.90 0.74 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19446 0 0 0 16837 80 0 0 25 0 1 0 1846531055 82481152 18669 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20137 18669 145 145 0 19992 0 [pid=8917] vsize: 80548 Current children cumulated CPU time (s) 169.18 Current children cumulated vsize (Kb) 82672 [startup+180.017 s] Raw data (loadavg): 0.97 0.90 0.74 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19624 0 0 0 17836 81 0 0 25 0 1 0 1846531055 82567168 18691 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20158 18691 145 145 0 20013 0 [pid=8917] vsize: 80632 Current children cumulated CPU time (s) 179.18 Current children cumulated vsize (Kb) 82756 [startup+190.018 s] Raw data (loadavg): 0.97 0.90 0.75 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19708 0 0 0 18834 83 0 0 25 0 1 0 1846531055 82759680 18742 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20205 18742 145 145 0 20060 0 [pid=8917] vsize: 80820 Current children cumulated CPU time (s) 189.18 Current children cumulated vsize (Kb) 82944 [startup+200.02 s] Raw data (loadavg): 0.98 0.91 0.75 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19774 0 0 0 19833 84 0 0 25 0 1 0 1846531055 82665472 18718 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20182 18718 145 145 0 20037 0 [pid=8917] vsize: 80728 Current children cumulated CPU time (s) 199.18 Current children cumulated vsize (Kb) 82852 [startup+210.021 s] Raw data (loadavg): 0.98 0.91 0.75 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19867 0 0 0 20832 85 0 0 25 0 1 0 1846531055 82669568 18720 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20183 18720 145 145 0 20038 0 [pid=8917] vsize: 80732 Current children cumulated CPU time (s) 209.18 Current children cumulated vsize (Kb) 82856 [startup+220.022 s] Raw data (loadavg): 0.98 0.91 0.75 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19871 0 0 0 21832 85 0 0 25 0 1 0 1846531055 82681856 18724 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20186 18724 145 145 0 20041 0 [pid=8917] vsize: 80744 Current children cumulated CPU time (s) 219.18 Current children cumulated vsize (Kb) 82868 [startup+230.022 s] Raw data (loadavg): 0.98 0.91 0.75 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19913 0 0 0 22832 85 0 0 25 0 1 0 1846531055 82853888 18766 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20228 18766 145 145 0 20083 0 [pid=8917] vsize: 80912 Current children cumulated CPU time (s) 229.18 Current children cumulated vsize (Kb) 83036 [startup+240.023 s] Raw data (loadavg): 0.99 0.92 0.75 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20020 0 0 0 23830 86 0 0 25 0 1 0 1846531055 82923520 18783 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20245 18783 145 145 0 20100 0 [pid=8917] vsize: 80980 Current children cumulated CPU time (s) 239.17 Current children cumulated vsize (Kb) 83104 [startup+250.023 s] Raw data (loadavg): 0.99 0.92 0.76 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20045 0 0 0 24830 86 0 0 25 0 1 0 1846531055 83021824 18808 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20269 18808 145 145 0 20124 0 [pid=8917] vsize: 81076 Current children cumulated CPU time (s) 249.17 Current children cumulated vsize (Kb) 83200 [startup+260.024 s] Raw data (loadavg): 0.99 0.92 0.76 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20057 0 0 0 25830 86 0 0 25 0 1 0 1846531055 83070976 18820 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20281 18820 145 145 0 20136 0 [pid=8917] vsize: 81124 Current children cumulated CPU time (s) 259.17 Current children cumulated vsize (Kb) 83248 [startup+270.024 s] Raw data (loadavg): 0.99 0.92 0.76 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20062 0 0 0 26830 86 0 0 25 0 1 0 1846531055 83091456 18825 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20286 18825 145 145 0 20141 0 [pid=8917] vsize: 81144 Current children cumulated CPU time (s) 269.17 Current children cumulated vsize (Kb) 83268 [startup+280.025 s] Raw data (loadavg): 0.99 0.92 0.76 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20090 0 0 0 27829 87 0 0 25 0 1 0 1846531055 83210240 18853 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20315 18853 145 145 0 20170 0 [pid=8917] vsize: 81260 Current children cumulated CPU time (s) 279.17 Current children cumulated vsize (Kb) 83384 [startup+290.025 s] Raw data (loadavg): 0.99 0.93 0.76 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20110 0 0 0 28829 87 0 0 25 0 1 0 1846531055 83283968 18873 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20333 18873 145 145 0 20188 0 [pid=8917] vsize: 81332 Current children cumulated CPU time (s) 289.17 Current children cumulated vsize (Kb) 83456 [startup+300.026 s] Raw data (loadavg): 0.99 0.93 0.77 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20130 0 0 0 29829 87 0 0 25 0 1 0 1846531055 83365888 18893 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20353 18893 145 145 0 20208 0 [pid=8917] vsize: 81412 Current children cumulated CPU time (s) 299.17 Current children cumulated vsize (Kb) 83536 [startup+310.027 s] Raw data (loadavg): 0.99 0.93 0.77 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20186 0 0 0 30829 88 0 0 25 0 1 0 1846531055 83697664 18949 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20434 18949 145 145 0 20289 0 [pid=8917] vsize: 81736 Current children cumulated CPU time (s) 309.18 Current children cumulated vsize (Kb) 83860 [startup+320.027 s] Raw data (loadavg): 0.99 0.93 0.77 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20190 0 0 0 31829 88 0 0 25 0 1 0 1846531055 83697664 18953 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20434 18953 145 145 0 20289 0 [pid=8917] vsize: 81736 Current children cumulated CPU time (s) 319.18 Current children cumulated vsize (Kb) 83860 [startup+330.029 s] Raw data (loadavg): 0.99 0.93 0.77 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20206 0 0 0 32829 88 0 0 25 0 1 0 1846531055 83750912 18969 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20447 18969 145 145 0 20302 0 [pid=8917] vsize: 81788 Current children cumulated CPU time (s) 329.18 Current children cumulated vsize (Kb) 83912 [startup+340.03 s] Raw data (loadavg): 0.99 0.94 0.77 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20223 0 0 0 33829 88 0 0 25 0 1 0 1846531055 83877888 18986 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20478 18986 145 145 0 20333 0 [pid=8917] vsize: 81912 Current children cumulated CPU time (s) 339.18 Current children cumulated vsize (Kb) 84036 [startup+350.031 s] Raw data (loadavg): 0.99 0.94 0.78 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20231 0 0 0 34829 88 0 0 25 0 1 0 1846531055 83910656 18994 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20486 18994 145 145 0 20341 0 [pid=8917] vsize: 81944 Current children cumulated CPU time (s) 349.18 Current children cumulated vsize (Kb) 84068 [startup+360.032 s] Raw data (loadavg): 0.99 0.94 0.78 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20276 0 0 0 35829 89 0 0 25 0 1 0 1846531055 84070400 19039 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20525 19039 145 145 0 20380 0 [pid=8917] vsize: 82100 Current children cumulated CPU time (s) 359.19 Current children cumulated vsize (Kb) 84224 [startup+370.032 s] Raw data (loadavg): 0.99 0.94 0.78 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20316 0 0 0 36829 89 0 0 25 0 1 0 1846531055 84238336 19079 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20566 19079 145 145 0 20421 0 [pid=8917] vsize: 82264 Current children cumulated CPU time (s) 369.19 Current children cumulated vsize (Kb) 84388 [startup+380.033 s] Raw data (loadavg): 0.99 0.94 0.78 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20416 0 0 0 37828 90 0 0 25 0 1 0 1846531055 84262912 19088 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20572 19088 145 145 0 20427 0 [pid=8917] vsize: 82288 Current children cumulated CPU time (s) 379.19 Current children cumulated vsize (Kb) 84412 [startup+390.033 s] Raw data (loadavg): 0.99 0.94 0.78 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20430 0 0 0 38828 90 0 0 25 0 1 0 1846531055 84320256 19102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20586 19102 145 145 0 20441 0 [pid=8917] vsize: 82344 Current children cumulated CPU time (s) 389.19 Current children cumulated vsize (Kb) 84468 [startup+400.034 s] Raw data (loadavg): 0.99 0.94 0.79 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20499 0 0 0 39828 90 0 0 25 0 1 0 1846531055 84467712 19138 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20622 19138 145 145 0 20477 0 [pid=8917] vsize: 82488 Current children cumulated CPU time (s) 399.19 Current children cumulated vsize (Kb) 84612 [startup+410.035 s] Raw data (loadavg): 0.99 0.95 0.79 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20530 0 0 0 40828 90 0 0 25 0 1 0 1846531055 84463616 19137 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20621 19137 145 145 0 20476 0 [pid=8917] vsize: 82484 Current children cumulated CPU time (s) 409.19 Current children cumulated vsize (Kb) 84608 [startup+420.035 s] Raw data (loadavg): 0.99 0.95 0.79 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20531 0 0 0 41828 90 0 0 25 0 1 0 1846531055 84463616 19138 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20621 19138 145 145 0 20476 0 [pid=8917] vsize: 82484 Current children cumulated CPU time (s) 419.19 Current children cumulated vsize (Kb) 84608 [startup+430.036 s] Raw data (loadavg): 0.99 0.95 0.79 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20535 0 0 0 42828 90 0 0 25 0 1 0 1846531055 84480000 19142 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20625 19142 145 145 0 20480 0 [pid=8917] vsize: 82500 Current children cumulated CPU time (s) 429.19 Current children cumulated vsize (Kb) 84624 [startup+440.037 s] Raw data (loadavg): 0.99 0.95 0.79 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20553 0 0 0 43828 91 0 0 25 0 1 0 1846531055 84553728 19160 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20643 19160 145 145 0 20498 0 [pid=8917] vsize: 82572 Current children cumulated CPU time (s) 439.2 Current children cumulated vsize (Kb) 84696 [startup+450.037 s] Raw data (loadavg): 0.99 0.95 0.80 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20564 0 0 0 44828 91 0 0 25 0 1 0 1846531055 84598784 19171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20654 19171 145 145 0 20509 0 [pid=8917] vsize: 82616 Current children cumulated CPU time (s) 449.2 Current children cumulated vsize (Kb) 84740 [startup+460.038 s] Raw data (loadavg): 0.99 0.95 0.80 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20574 0 0 0 45828 91 0 0 25 0 1 0 1846531055 84643840 19181 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20665 19181 145 145 0 20520 0 [pid=8917] vsize: 82660 Current children cumulated CPU time (s) 459.2 Current children cumulated vsize (Kb) 84784 [startup+470.039 s] Raw data (loadavg): 0.99 0.95 0.80 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20667 0 0 0 46827 92 0 0 25 0 1 0 1846531055 84652032 19184 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20667 19184 145 145 0 20522 0 [pid=8917] vsize: 82668 Current children cumulated CPU time (s) 469.2 Current children cumulated vsize (Kb) 84792 [startup+480.04 s] Raw data (loadavg): 0.99 0.95 0.80 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20673 0 0 0 47827 92 0 0 25 0 1 0 1846531055 84676608 19190 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20673 19190 145 145 0 20528 0 [pid=8917] vsize: 82692 Current children cumulated CPU time (s) 479.2 Current children cumulated vsize (Kb) 84816 [startup+490.041 s] Raw data (loadavg): 0.99 0.95 0.80 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20690 0 0 0 48828 92 0 0 25 0 1 0 1846531055 84758528 19207 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20693 19207 145 145 0 20548 0 [pid=8917] vsize: 82772 Current children cumulated CPU time (s) 489.21 Current children cumulated vsize (Kb) 84896 [startup+500.042 s] Raw data (loadavg): 0.99 0.95 0.81 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20702 0 0 0 49828 92 0 0 25 0 1 0 1846531055 84795392 19219 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20702 19219 145 145 0 20557 0 [pid=8917] vsize: 82808 Current children cumulated CPU time (s) 499.21 Current children cumulated vsize (Kb) 84932 [startup+510.042 s] Raw data (loadavg): 0.99 0.96 0.81 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20724 0 0 0 50828 92 0 0 25 0 1 0 1846531055 84881408 19241 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20723 19241 145 145 0 20578 0 [pid=8917] vsize: 82892 Current children cumulated CPU time (s) 509.21 Current children cumulated vsize (Kb) 85016 [startup+520.042 s] Raw data (loadavg): 0.99 0.96 0.81 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20752 0 0 0 51828 92 0 0 25 0 1 0 1846531055 84996096 19269 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20751 19269 145 145 0 20606 0 [pid=8917] vsize: 83004 Current children cumulated CPU time (s) 519.21 Current children cumulated vsize (Kb) 85128 [startup+530.044 s] Raw data (loadavg): 0.99 0.96 0.81 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20765 0 0 0 52828 92 0 0 25 0 1 0 1846531055 85049344 19282 4294967295 134512640 135094434 3221224432 3221223056 134557645 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20764 19282 145 145 0 20619 0 [pid=8917] vsize: 83056 Current children cumulated CPU time (s) 529.21 Current children cumulated vsize (Kb) 85180 [startup+540.045 s] Raw data (loadavg): 0.99 0.96 0.81 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20772 0 0 0 53828 92 0 0 25 0 1 0 1846531055 85073920 19289 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20770 19289 145 145 0 20625 0 [pid=8917] vsize: 83080 Current children cumulated CPU time (s) 539.21 Current children cumulated vsize (Kb) 85204 [startup+550.045 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20806 0 0 0 54828 92 0 0 25 0 1 0 1846531055 85213184 19323 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20804 19323 145 145 0 20659 0 [pid=8917] vsize: 83216 Current children cumulated CPU time (s) 549.21 Current children cumulated vsize (Kb) 85340 [startup+560.046 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20917 0 0 0 55827 93 0 0 25 0 1 0 1846531055 85299200 19343 4294967295 134512640 135094434 3221224432 3221223184 134559512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20825 19343 145 145 0 20680 0 [pid=8917] vsize: 83300 Current children cumulated CPU time (s) 559.21 Current children cumulated vsize (Kb) 85424 [startup+570.047 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21009 0 0 0 56827 93 0 0 25 0 1 0 1846531055 85295104 19343 4294967295 134512640 135094434 3221224432 3221223104 134555566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20824 19343 145 145 0 20679 0 [pid=8917] vsize: 83296 Current children cumulated CPU time (s) 569.21 Current children cumulated vsize (Kb) 85420 [startup+580.047 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21023 0 0 0 57827 93 0 0 25 0 1 0 1846531055 85352448 19357 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20838 19357 145 145 0 20693 0 [pid=8917] vsize: 83352 Current children cumulated CPU time (s) 579.21 Current children cumulated vsize (Kb) 85476 [startup+590.048 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21038 0 0 0 58827 93 0 0 25 0 1 0 1846531055 85409792 19372 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20852 19372 145 145 0 20707 0 [pid=8917] vsize: 83408 Current children cumulated CPU time (s) 589.21 Current children cumulated vsize (Kb) 85532 [startup+600.049 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21053 0 0 0 59827 94 0 0 25 0 1 0 1846531055 85471232 19387 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20867 19387 145 145 0 20722 0 [pid=8917] vsize: 83468 Current children cumulated CPU time (s) 599.22 Current children cumulated vsize (Kb) 85592 [startup+610.049 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21087 0 0 0 60827 94 0 0 25 0 1 0 1846531055 85614592 19421 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20902 19421 145 145 0 20757 0 [pid=8917] vsize: 83608 Current children cumulated CPU time (s) 609.22 Current children cumulated vsize (Kb) 85732 [startup+620.05 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21128 0 0 0 61826 94 0 0 25 0 1 0 1846531055 85778432 19462 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20942 19462 145 145 0 20797 0 [pid=8917] vsize: 83768 Current children cumulated CPU time (s) 619.21 Current children cumulated vsize (Kb) 85892 [startup+630.051 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21142 0 0 0 62826 94 0 0 25 0 1 0 1846531055 85831680 19476 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20955 19476 145 145 0 20810 0 [pid=8917] vsize: 83820 Current children cumulated CPU time (s) 629.21 Current children cumulated vsize (Kb) 85944 [startup+640.051 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21158 0 0 0 63826 94 0 0 25 0 1 0 1846531055 85897216 19492 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20971 19492 145 145 0 20826 0 [pid=8917] vsize: 83884 Current children cumulated CPU time (s) 639.21 Current children cumulated vsize (Kb) 86008 [startup+650.052 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21173 0 0 0 64826 95 0 0 25 0 1 0 1846531055 85962752 19507 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20987 19507 145 145 0 20842 0 [pid=8917] vsize: 83948 Current children cumulated CPU time (s) 649.22 Current children cumulated vsize (Kb) 86072 [startup+660.053 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21185 0 0 0 65826 95 0 0 25 0 1 0 1846531055 86003712 19519 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 20997 19519 145 145 0 20852 0 [pid=8917] vsize: 83988 Current children cumulated CPU time (s) 659.22 Current children cumulated vsize (Kb) 86112 [startup+670.053 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21201 0 0 0 66826 95 0 0 25 0 1 0 1846531055 86089728 19535 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21018 19535 145 145 0 20873 0 [pid=8917] vsize: 84072 Current children cumulated CPU time (s) 669.22 Current children cumulated vsize (Kb) 86196 [startup+680.054 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21300 0 0 0 67825 95 0 0 25 0 1 0 1846531055 86102016 19543 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21021 19543 145 145 0 20876 0 [pid=8917] vsize: 84084 Current children cumulated CPU time (s) 679.21 Current children cumulated vsize (Kb) 86208 [startup+690.055 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21312 0 0 0 68825 95 0 0 25 0 1 0 1846531055 86155264 19555 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21034 19555 145 145 0 20889 0 [pid=8917] vsize: 84136 Current children cumulated CPU time (s) 689.21 Current children cumulated vsize (Kb) 86260 [startup+700.054 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21333 0 0 0 69825 96 0 0 25 0 1 0 1846531055 86241280 19576 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21055 19576 145 145 0 20910 0 [pid=8917] vsize: 84220 Current children cumulated CPU time (s) 699.22 Current children cumulated vsize (Kb) 86344 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21357 0 0 0 70825 96 0 0 25 0 1 0 1846531055 86331392 19600 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21077 19600 145 145 0 20932 0 [pid=8917] vsize: 84308 Current children cumulated CPU time (s) 709.22 Current children cumulated vsize (Kb) 86432 [startup+720.057 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21376 0 0 0 71825 96 0 0 25 0 1 0 1846531055 86409216 19619 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21096 19619 145 145 0 20951 0 [pid=8917] vsize: 84384 Current children cumulated CPU time (s) 719.22 Current children cumulated vsize (Kb) 86508 [startup+730.058 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21444 0 0 0 72825 96 0 0 25 0 1 0 1846531055 86528000 19648 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21125 19648 145 145 0 20980 0 [pid=8917] vsize: 84500 Current children cumulated CPU time (s) 729.22 Current children cumulated vsize (Kb) 86624 [startup+740.058 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21485 0 0 0 73825 96 0 0 25 0 1 0 1846531055 86487040 19638 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21115 19638 145 145 0 20970 0 [pid=8917] vsize: 84460 Current children cumulated CPU time (s) 739.22 Current children cumulated vsize (Kb) 86584 [startup+750.059 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21497 0 0 0 74825 96 0 0 25 0 1 0 1846531055 86536192 19650 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21127 19650 145 145 0 20982 0 [pid=8917] vsize: 84508 Current children cumulated CPU time (s) 749.22 Current children cumulated vsize (Kb) 86632 [startup+760.059 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21512 0 0 0 75825 97 0 0 25 0 1 0 1846531055 86593536 19665 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21141 19665 145 145 0 20996 0 [pid=8917] vsize: 84564 Current children cumulated CPU time (s) 759.23 Current children cumulated vsize (Kb) 86688 [startup+770.06 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21521 0 0 0 76825 97 0 0 25 0 1 0 1846531055 86626304 19674 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21149 19674 145 145 0 21004 0 [pid=8917] vsize: 84596 Current children cumulated CPU time (s) 769.23 Current children cumulated vsize (Kb) 86720 [startup+780.062 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21533 0 0 0 77825 97 0 0 25 0 1 0 1846531055 86679552 19686 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21162 19686 145 145 0 21017 0 [pid=8917] vsize: 84648 Current children cumulated CPU time (s) 779.23 Current children cumulated vsize (Kb) 86772 [startup+790.062 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21549 0 0 0 78824 98 0 0 25 0 1 0 1846531055 86740992 19702 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21177 19702 145 145 0 21032 0 [pid=8917] vsize: 84708 Current children cumulated CPU time (s) 789.23 Current children cumulated vsize (Kb) 86832 [startup+800.063 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21649 0 0 0 79823 99 0 0 25 0 1 0 1846531055 86777856 19711 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21186 19711 145 145 0 21041 0 [pid=8917] vsize: 84744 Current children cumulated CPU time (s) 799.23 Current children cumulated vsize (Kb) 86868 [startup+810.065 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21670 0 0 0 80822 100 0 0 25 0 1 0 1846531055 86855680 19732 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21205 19732 145 145 0 21060 0 [pid=8917] vsize: 84820 Current children cumulated CPU time (s) 809.23 Current children cumulated vsize (Kb) 86944 [startup+820.066 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21685 0 0 0 81822 100 0 0 25 0 1 0 1846531055 86921216 19747 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21221 19747 145 145 0 21076 0 [pid=8917] vsize: 84884 Current children cumulated CPU time (s) 819.23 Current children cumulated vsize (Kb) 87008 [startup+830.066 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21702 0 0 0 82822 100 0 0 25 0 1 0 1846531055 86986752 19764 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21237 19764 145 145 0 21092 0 [pid=8917] vsize: 84948 Current children cumulated CPU time (s) 829.23 Current children cumulated vsize (Kb) 87072 [startup+840.067 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21810 0 0 0 83821 101 0 0 25 0 1 0 1846531055 87060480 19780 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21255 19780 145 145 0 21110 0 [pid=8917] vsize: 85020 Current children cumulated CPU time (s) 839.23 Current children cumulated vsize (Kb) 87144 [startup+850.068 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21893 0 0 0 84820 102 0 0 25 0 1 0 1846531055 87248896 19830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21301 19830 145 145 0 21156 0 [pid=8917] vsize: 85204 Current children cumulated CPU time (s) 849.23 Current children cumulated vsize (Kb) 87328 [startup+860.068 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21910 0 0 0 85820 102 0 0 25 0 1 0 1846531055 87318528 19847 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19847 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 859.23 Current children cumulated vsize (Kb) 87396 [startup+870.069 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 86821 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 869.24 Current children cumulated vsize (Kb) 87396 [startup+880.07 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 87820 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 879.23 Current children cumulated vsize (Kb) 87396 [startup+890.07 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 88821 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 889.24 Current children cumulated vsize (Kb) 87396 [startup+900.071 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 89820 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 899.23 Current children cumulated vsize (Kb) 87396 [startup+910.072 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21912 0 0 0 90821 102 0 0 25 0 1 0 1846531055 87318528 19849 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19849 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 909.24 Current children cumulated vsize (Kb) 87396 [startup+920.072 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21912 0 0 0 91821 102 0 0 25 0 1 0 1846531055 87318528 19849 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19849 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 919.24 Current children cumulated vsize (Kb) 87396 [startup+930.073 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21912 0 0 0 92821 102 0 0 25 0 1 0 1846531055 87318528 19849 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21318 19849 145 145 0 21173 0 [pid=8917] vsize: 85272 Current children cumulated CPU time (s) 929.24 Current children cumulated vsize (Kb) 87396 [startup+940.074 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21921 0 0 0 93821 103 0 0 25 0 1 0 1846531055 87355392 19858 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21327 19858 145 145 0 21182 0 [pid=8917] vsize: 85308 Current children cumulated CPU time (s) 939.25 Current children cumulated vsize (Kb) 87432 [startup+950.074 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21941 0 0 0 94821 103 0 0 25 0 1 0 1846531055 87433216 19878 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21346 19878 145 145 0 21201 0 [pid=8917] vsize: 85384 Current children cumulated CPU time (s) 949.25 Current children cumulated vsize (Kb) 87508 [startup+960.075 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21952 0 0 0 95821 103 0 0 25 0 1 0 1846531055 87482368 19889 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21358 19889 145 145 0 21213 0 [pid=8917] vsize: 85432 Current children cumulated CPU time (s) 959.25 Current children cumulated vsize (Kb) 87556 [startup+970.076 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22023 0 0 0 96821 103 0 0 25 0 1 0 1846531055 87609344 19921 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21389 19921 145 145 0 21244 0 [pid=8917] vsize: 85556 Current children cumulated CPU time (s) 969.25 Current children cumulated vsize (Kb) 87680 [startup+980.077 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22120 0 0 0 97820 104 0 0 25 0 1 0 1846531055 87638016 19928 4294967295 134512640 135094434 3221224432 3221220284 134676460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21396 19928 145 145 0 21251 0 [pid=8917] vsize: 85584 Current children cumulated CPU time (s) 979.25 Current children cumulated vsize (Kb) 87708 [startup+990.077 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22160 0 0 0 98820 104 0 0 25 0 1 0 1846531055 87584768 19916 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21383 19916 145 145 0 21238 0 [pid=8917] vsize: 85532 Current children cumulated CPU time (s) 989.25 Current children cumulated vsize (Kb) 87656 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22168 0 0 0 99820 105 0 0 25 0 1 0 1846531055 87617536 19924 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21391 19924 145 145 0 21246 0 [pid=8917] vsize: 85564 Current children cumulated CPU time (s) 999.26 Current children cumulated vsize (Kb) 87688 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22182 0 0 0 100820 105 0 0 25 0 1 0 1846531055 87678976 19938 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21406 19938 145 145 0 21261 0 [pid=8917] vsize: 85624 Current children cumulated CPU time (s) 1009.26 Current children cumulated vsize (Kb) 87748 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22200 0 0 0 101819 105 0 0 25 0 1 0 1846531055 87752704 19956 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21424 19956 145 145 0 21279 0 [pid=8917] vsize: 85696 Current children cumulated CPU time (s) 1019.25 Current children cumulated vsize (Kb) 87820 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22212 0 0 0 102820 105 0 0 25 0 1 0 1846531055 87793664 19968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21434 19968 145 145 0 21289 0 [pid=8917] vsize: 85736 Current children cumulated CPU time (s) 1029.26 Current children cumulated vsize (Kb) 87860 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22229 0 0 0 103820 105 0 0 25 0 1 0 1846531055 87863296 19985 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21451 19985 145 145 0 21306 0 [pid=8917] vsize: 85804 Current children cumulated CPU time (s) 1039.26 Current children cumulated vsize (Kb) 87928 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22241 0 0 0 104820 105 0 0 25 0 1 0 1846531055 87912448 19997 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21463 19997 145 145 0 21318 0 [pid=8917] vsize: 85852 Current children cumulated CPU time (s) 1049.26 Current children cumulated vsize (Kb) 87976 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22253 0 0 0 105820 105 0 0 25 0 1 0 1846531055 87961600 20009 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21475 20009 145 145 0 21330 0 [pid=8917] vsize: 85900 Current children cumulated CPU time (s) 1059.26 Current children cumulated vsize (Kb) 88024 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22297 0 0 0 106820 105 0 0 25 0 1 0 1846531055 88272896 20053 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21551 20053 145 145 0 21406 0 [pid=8917] vsize: 86204 Current children cumulated CPU time (s) 1069.26 Current children cumulated vsize (Kb) 88328 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22297 0 0 0 107820 105 0 0 25 0 1 0 1846531055 88272896 20053 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21551 20053 145 145 0 21406 0 [pid=8917] vsize: 86204 Current children cumulated CPU time (s) 1079.26 Current children cumulated vsize (Kb) 88328 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22297 0 0 0 108820 105 0 0 25 0 1 0 1846531055 88272896 20053 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21551 20053 145 145 0 21406 0 [pid=8917] vsize: 86204 Current children cumulated CPU time (s) 1089.26 Current children cumulated vsize (Kb) 88328 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22303 0 0 0 109821 105 0 0 25 0 1 0 1846531055 88293376 20059 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21556 20059 145 145 0 21411 0 [pid=8917] vsize: 86224 Current children cumulated CPU time (s) 1099.27 Current children cumulated vsize (Kb) 88348 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 8917 Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/8913/statm): 531 226 485 147 0 384 0 [pid=8913] vsize: 2124 Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22317 0 0 0 110820 106 0 0 25 0 1 0 1846531055 88346624 20073 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8917/statm): 21569 20073 145 145 0 21424 0 [pid=8917] vsize: 86276 Current children cumulated CPU time (s) 1109.27 Current children cumulated vsize (Kb) 88400 One traced child (pid=8917) exited with status: 30 One traced child (pid=8913) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 1119.21 CPU time (s): 1118.41 CPU user time (s): 1117.29 CPU system time (s): 1.12183 CPU usage (%): 99.929 Max. virtual memory (cumulated for all children) (Kb): 88400
Verifier: OK 471047168