Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-egout.opb |
MD5SUM | 99bcb41cf234e24f89287b787fc4273a |
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 | 1108.66 |
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 17:46:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2968 boxname=wulflinc26 idbench=624 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 99bcb41cf234e24f89287b787fc4273a /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: 2968 /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: 859224 kB Buffers: 38280 kB Cached: 108616 kB SwapCached: 868 kB Active: 81020 kB Inactive: 68528 kB HighTotal: 131008 kB HighFree: 26432 kB LowTotal: 903652 kB LowFree: 832792 kB SwapTotal: 2097892 kB SwapFree: 2096540 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5704 kB Slab: 20408 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:04:31 (client local time) WITH STATUS 30 IN 1108.66 SECONDS stats: 2968 0 1108.66 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 (123 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 1107.27 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/11520/stat): 11520 (minisat+_script) R 11519 11520 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851813923 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/11520/statm): 174 3 169 147 0 27 0 [pid=11520] 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=11521 New process pid=11522 New process pid=11523 execve syscall for /bin/sed executable One traced child (pid=11522) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=11523) exited with status: 0 One traced child (pid=11521) exited with status: 0 New process pid=11524 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.0042 s] Raw data (loadavg): 0.71 0.89 0.68 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 9744 0 2 0 901 40 0 0 25 0 1 0 1851813928 41115648 9428 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 10038 9428 145 145 0 9893 0 [pid=11524] vsize: 40152 Current children cumulated CPU time (s) 9.42 Current children cumulated vsize (Kb) 42276 [startup+20.0049 s] Raw data (loadavg): 0.75 0.90 0.69 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 9783 0 2 0 1900 41 0 0 25 0 1 0 1851813928 41209856 9467 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 10061 9467 145 145 0 9916 0 [pid=11524] vsize: 40244 Current children cumulated CPU time (s) 19.42 Current children cumulated vsize (Kb) 42368 [startup+30.0066 s] Raw data (loadavg): 0.79 0.90 0.69 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 10060 0 2 0 2898 42 0 0 25 0 1 0 1851813928 42332160 9744 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 10335 9744 145 145 0 10190 0 [pid=11524] vsize: 41340 Current children cumulated CPU time (s) 29.41 Current children cumulated vsize (Kb) 43464 [startup+40.0072 s] Raw data (loadavg): 0.82 0.90 0.69 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14511 0 2 0 3864 59 0 0 25 0 1 0 1851813928 65654784 13827 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 16029 13827 145 145 0 15884 0 [pid=11524] vsize: 64116 Current children cumulated CPU time (s) 39.24 Current children cumulated vsize (Kb) 66240 [startup+50.0089 s] Raw data (loadavg): 0.85 0.91 0.70 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14595 0 2 0 4864 60 0 0 25 0 1 0 1851813928 65925120 13911 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 16095 13911 145 145 0 15950 0 [pid=11524] vsize: 64380 Current children cumulated CPU time (s) 49.25 Current children cumulated vsize (Kb) 66504 [startup+60.0096 s] Raw data (loadavg): 0.87 0.91 0.70 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14655 0 2 0 5864 60 0 0 25 0 1 0 1851813928 66101248 13971 4294967295 134512640 135094434 3221224432 3221223104 134555447 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 16138 13971 145 145 0 15993 0 [pid=11524] vsize: 64552 Current children cumulated CPU time (s) 59.25 Current children cumulated vsize (Kb) 66676 [startup+70.0103 s] Raw data (loadavg): 0.89 0.91 0.70 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14774 0 2 0 6862 61 0 0 25 0 1 0 1851813928 66580480 14090 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 16255 14090 145 145 0 16110 0 [pid=11524] vsize: 65020 Current children cumulated CPU time (s) 69.24 Current children cumulated vsize (Kb) 67144 [startup+80.0119 s] Raw data (loadavg): 0.91 0.91 0.70 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14990 0 2 0 7861 62 0 0 25 0 1 0 1851813928 67129344 14306 4294967295 134512640 135094434 3221224432 3221221984 134677333 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 16389 14306 145 145 0 16244 0 [pid=11524] vsize: 65556 Current children cumulated CPU time (s) 79.24 Current children cumulated vsize (Kb) 67680 [startup+90.0127 s] Raw data (loadavg): 0.92 0.92 0.71 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 18996 0 2 0 8826 80 0 0 25 0 1 0 1851813928 80711680 18312 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 19705 18312 145 145 0 19560 0 [pid=11524] vsize: 78820 Current children cumulated CPU time (s) 89.07 Current children cumulated vsize (Kb) 80944 [startup+100.014 s] Raw data (loadavg): 0.93 0.92 0.71 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19002 0 2 0 9827 80 0 0 25 0 1 0 1851813928 80736256 18318 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 19711 18318 145 145 0 19566 0 [pid=11524] vsize: 78844 Current children cumulated CPU time (s) 99.08 Current children cumulated vsize (Kb) 80968 [startup+110.016 s] Raw data (loadavg): 0.94 0.92 0.71 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19009 0 2 0 10826 80 0 0 25 0 1 0 1851813928 80764928 18325 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 19718 18325 145 145 0 19573 0 [pid=11524] vsize: 78872 Current children cumulated CPU time (s) 109.07 Current children cumulated vsize (Kb) 80996 [startup+120.017 s] Raw data (loadavg): 0.95 0.92 0.72 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19030 0 2 0 11825 81 0 0 25 0 1 0 1851813928 80879616 18346 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 19746 18346 145 145 0 19601 0 [pid=11524] vsize: 78984 Current children cumulated CPU time (s) 119.07 Current children cumulated vsize (Kb) 81108 [startup+130.018 s] Raw data (loadavg): 0.96 0.92 0.72 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19076 0 2 0 12824 81 0 0 25 0 1 0 1851813928 81104896 18392 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 19801 18392 145 145 0 19656 0 [pid=11524] vsize: 79204 Current children cumulated CPU time (s) 129.06 Current children cumulated vsize (Kb) 81328 [startup+140.019 s] Raw data (loadavg): 0.96 0.93 0.72 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19301 0 2 0 13822 83 0 0 25 0 1 0 1851813928 82276352 18617 4294967295 134512640 135094434 3221224432 3221221632 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20087 18617 145 145 0 19942 0 [pid=11524] vsize: 80348 Current children cumulated CPU time (s) 139.06 Current children cumulated vsize (Kb) 82472 [startup+150.021 s] Raw data (loadavg): 0.97 0.93 0.72 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19313 0 2 0 14822 83 0 0 25 0 1 0 1851813928 82317312 18629 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20097 18629 145 145 0 19952 0 [pid=11524] vsize: 80388 Current children cumulated CPU time (s) 149.06 Current children cumulated vsize (Kb) 82512 [startup+160.021 s] Raw data (loadavg): 0.97 0.93 0.73 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19330 0 2 0 15821 84 0 0 25 0 1 0 1851813928 82386944 18646 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20114 18646 145 145 0 19969 0 [pid=11524] vsize: 80456 Current children cumulated CPU time (s) 159.06 Current children cumulated vsize (Kb) 82580 [startup+170.022 s] Raw data (loadavg): 0.98 0.93 0.73 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19501 0 2 0 16819 85 0 0 25 0 1 0 1851813928 82550784 18687 4294967295 134512640 135094434 3221224432 3221220496 134677138 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20154 18687 145 145 0 20009 0 [pid=11524] vsize: 80616 Current children cumulated CPU time (s) 169.05 Current children cumulated vsize (Kb) 82740 [startup+180.023 s] Raw data (loadavg): 0.98 0.93 0.73 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19622 0 2 0 17817 86 0 0 25 0 1 0 1851813928 82567168 18691 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20158 18691 145 145 0 20013 0 [pid=11524] vsize: 80632 Current children cumulated CPU time (s) 179.04 Current children cumulated vsize (Kb) 82756 [startup+190.024 s] Raw data (loadavg): 0.98 0.94 0.73 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19706 0 2 0 18816 87 0 0 25 0 1 0 1851813928 82759680 18742 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20205 18742 145 145 0 20060 0 [pid=11524] vsize: 80820 Current children cumulated CPU time (s) 189.04 Current children cumulated vsize (Kb) 82944 [startup+200.026 s] Raw data (loadavg): 0.98 0.94 0.74 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19772 0 2 0 19815 87 0 0 25 0 1 0 1851813928 82665472 18718 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20182 18718 145 145 0 20037 0 [pid=11524] vsize: 80728 Current children cumulated CPU time (s) 199.03 Current children cumulated vsize (Kb) 82852 [startup+210.027 s] Raw data (loadavg): 0.99 0.94 0.74 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19865 0 2 0 20814 88 0 0 25 0 1 0 1851813928 82669568 18720 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20183 18720 145 145 0 20038 0 [pid=11524] vsize: 80732 Current children cumulated CPU time (s) 209.03 Current children cumulated vsize (Kb) 82856 [startup+220.028 s] Raw data (loadavg): 0.99 0.94 0.74 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19883 0 2 0 21813 89 0 0 25 0 1 0 1851813928 82739200 18738 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20200 18738 145 145 0 20055 0 [pid=11524] vsize: 80800 Current children cumulated CPU time (s) 219.03 Current children cumulated vsize (Kb) 82924 [startup+230.029 s] Raw data (loadavg): 0.99 0.94 0.74 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19914 0 2 0 22813 89 0 0 25 0 1 0 1851813928 82866176 18769 4294967295 134512640 135094434 3221224432 3221223072 134562063 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20231 18769 145 145 0 20086 0 [pid=11524] vsize: 80924 Current children cumulated CPU time (s) 229.03 Current children cumulated vsize (Kb) 83048 [startup+240.03 s] Raw data (loadavg): 0.99 0.94 0.74 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20026 0 2 0 23811 90 0 0 25 0 1 0 1851813928 82956288 18791 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20253 18791 145 145 0 20108 0 [pid=11524] vsize: 81012 Current children cumulated CPU time (s) 239.02 Current children cumulated vsize (Kb) 83136 [startup+250.032 s] Raw data (loadavg): 0.99 0.94 0.75 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20045 0 2 0 24810 91 0 0 25 0 1 0 1851813928 83030016 18810 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20271 18810 145 145 0 20126 0 [pid=11524] vsize: 81084 Current children cumulated CPU time (s) 249.02 Current children cumulated vsize (Kb) 83208 [startup+260.033 s] Raw data (loadavg): 0.99 0.95 0.75 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20057 0 2 0 25809 92 0 0 25 0 1 0 1851813928 83079168 18822 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20283 18822 145 145 0 20138 0 [pid=11524] vsize: 81132 Current children cumulated CPU time (s) 259.02 Current children cumulated vsize (Kb) 83256 [startup+270.034 s] Raw data (loadavg): 0.99 0.95 0.75 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20062 0 2 0 26809 92 0 0 25 0 1 0 1851813928 83099648 18827 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20288 18827 145 145 0 20143 0 [pid=11524] vsize: 81152 Current children cumulated CPU time (s) 269.02 Current children cumulated vsize (Kb) 83276 [startup+280.036 s] Raw data (loadavg): 0.99 0.95 0.75 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20097 0 2 0 27808 92 0 0 25 0 1 0 1851813928 83238912 18862 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20322 18862 145 145 0 20177 0 [pid=11524] vsize: 81288 Current children cumulated CPU time (s) 279.01 Current children cumulated vsize (Kb) 83412 [startup+290.037 s] Raw data (loadavg): 0.99 0.95 0.75 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20111 0 2 0 28808 93 0 0 25 0 1 0 1851813928 83296256 18876 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20336 18876 145 145 0 20191 0 [pid=11524] vsize: 81344 Current children cumulated CPU time (s) 289.02 Current children cumulated vsize (Kb) 83468 [startup+300.038 s] Raw data (loadavg): 0.99 0.95 0.75 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20133 0 2 0 29807 93 0 0 25 0 1 0 1851813928 83390464 18898 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20359 18898 145 145 0 20214 0 [pid=11524] vsize: 81436 Current children cumulated CPU time (s) 299.01 Current children cumulated vsize (Kb) 83560 [startup+310.039 s] Raw data (loadavg): 0.99 0.95 0.76 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20184 0 2 0 30807 94 0 0 25 0 1 0 1851813928 83697664 18949 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20434 18949 145 145 0 20289 0 [pid=11524] vsize: 81736 Current children cumulated CPU time (s) 309.02 Current children cumulated vsize (Kb) 83860 [startup+320.039 s] Raw data (loadavg): 0.99 0.95 0.76 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20188 0 2 0 31807 94 0 0 25 0 1 0 1851813928 83697664 18953 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20434 18953 145 145 0 20289 0 [pid=11524] vsize: 81736 Current children cumulated CPU time (s) 319.02 Current children cumulated vsize (Kb) 83860 [startup+330.041 s] Raw data (loadavg): 0.99 0.95 0.76 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20204 0 2 0 32806 94 0 0 25 0 1 0 1851813928 83750912 18969 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20447 18969 145 145 0 20302 0 [pid=11524] vsize: 81788 Current children cumulated CPU time (s) 329.01 Current children cumulated vsize (Kb) 83912 [startup+340.042 s] Raw data (loadavg): 0.99 0.95 0.76 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20221 0 2 0 33806 95 0 0 25 0 1 0 1851813928 83877888 18986 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20478 18986 145 145 0 20333 0 [pid=11524] vsize: 81912 Current children cumulated CPU time (s) 339.02 Current children cumulated vsize (Kb) 84036 [startup+350.043 s] Raw data (loadavg): 0.99 0.95 0.76 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20245 0 2 0 34805 96 0 0 25 0 1 0 1851813928 83976192 19010 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20502 19010 145 145 0 20357 0 [pid=11524] vsize: 82008 Current children cumulated CPU time (s) 349.02 Current children cumulated vsize (Kb) 84132 [startup+360.044 s] Raw data (loadavg): 0.99 0.95 0.77 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20288 0 2 0 35805 96 0 0 25 0 1 0 1851813928 84123648 19053 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20538 19053 145 145 0 20393 0 [pid=11524] vsize: 82152 Current children cumulated CPU time (s) 359.02 Current children cumulated vsize (Kb) 84276 [startup+370.045 s] Raw data (loadavg): 0.99 0.96 0.77 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20374 0 2 0 36804 97 0 0 25 0 1 0 1851813928 84316160 19100 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20585 19100 145 145 0 20440 0 [pid=11524] vsize: 82340 Current children cumulated CPU time (s) 369.02 Current children cumulated vsize (Kb) 84464 [startup+380.046 s] Raw data (loadavg): 0.99 0.96 0.77 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20419 0 2 0 37803 97 0 0 25 0 1 0 1851813928 84283392 19093 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20577 19093 145 145 0 20432 0 [pid=11524] vsize: 82308 Current children cumulated CPU time (s) 379.01 Current children cumulated vsize (Kb) 84432 [startup+390.047 s] Raw data (loadavg): 0.99 0.96 0.77 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20435 0 2 0 38802 98 0 0 25 0 1 0 1851813928 84348928 19109 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20593 19109 145 145 0 20448 0 [pid=11524] vsize: 82372 Current children cumulated CPU time (s) 389.01 Current children cumulated vsize (Kb) 84496 [startup+400.049 s] Raw data (loadavg): 0.99 0.96 0.77 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20528 0 2 0 39801 99 0 0 25 0 1 0 1851813928 84463616 19137 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20621 19137 145 145 0 20476 0 [pid=11524] vsize: 82484 Current children cumulated CPU time (s) 399.01 Current children cumulated vsize (Kb) 84608 [startup+410.049 s] Raw data (loadavg): 0.99 0.96 0.78 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20528 0 2 0 40800 99 0 0 25 0 1 0 1851813928 84463616 19137 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20621 19137 145 145 0 20476 0 [pid=11524] vsize: 82484 Current children cumulated CPU time (s) 409 Current children cumulated vsize (Kb) 84608 [startup+420.05 s] Raw data (loadavg): 0.99 0.96 0.78 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20533 0 2 0 41800 100 0 0 25 0 1 0 1851813928 84480000 19142 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20625 19142 145 145 0 20480 0 [pid=11524] vsize: 82500 Current children cumulated CPU time (s) 419.01 Current children cumulated vsize (Kb) 84624 [startup+430.052 s] Raw data (loadavg): 0.99 0.96 0.78 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20541 0 2 0 42799 100 0 0 25 0 1 0 1851813928 84512768 19150 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20633 19150 145 145 0 20488 0 [pid=11524] vsize: 82532 Current children cumulated CPU time (s) 429 Current children cumulated vsize (Kb) 84656 [startup+440.052 s] Raw data (loadavg): 0.99 0.96 0.78 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20557 0 2 0 43798 101 0 0 25 0 1 0 1851813928 84578304 19166 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20649 19166 145 145 0 20504 0 [pid=11524] vsize: 82596 Current children cumulated CPU time (s) 439 Current children cumulated vsize (Kb) 84720 [startup+450.053 s] Raw data (loadavg): 0.99 0.96 0.78 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20567 0 2 0 44798 101 0 0 25 0 1 0 1851813928 84627456 19176 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20661 19176 145 145 0 20516 0 [pid=11524] vsize: 82644 Current children cumulated CPU time (s) 449 Current children cumulated vsize (Kb) 84768 [startup+460.054 s] Raw data (loadavg): 0.99 0.96 0.79 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20635 0 2 0 45797 102 0 0 25 0 1 0 1851813928 84738048 19205 4294967295 134512640 135094434 3221224432 3221219944 134677084 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20688 19205 145 145 0 20543 0 [pid=11524] vsize: 82752 Current children cumulated CPU time (s) 459 Current children cumulated vsize (Kb) 84876 [startup+470.055 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20668 0 2 0 46796 103 0 0 25 0 1 0 1851813928 84668416 19187 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20671 19187 145 145 0 20526 0 [pid=11524] vsize: 82684 Current children cumulated CPU time (s) 469 Current children cumulated vsize (Kb) 84808 [startup+480.055 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20676 0 2 0 47796 103 0 0 25 0 1 0 1851813928 84697088 19195 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20678 19195 145 145 0 20533 0 [pid=11524] vsize: 82712 Current children cumulated CPU time (s) 479 Current children cumulated vsize (Kb) 84836 [startup+490.056 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20690 0 2 0 48796 103 0 0 25 0 1 0 1851813928 84758528 19209 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20693 19209 145 145 0 20548 0 [pid=11524] vsize: 82772 Current children cumulated CPU time (s) 489 Current children cumulated vsize (Kb) 84896 [startup+500.058 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20707 0 2 0 49795 104 0 0 25 0 1 0 1851813928 84819968 19226 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20708 19226 145 145 0 20563 0 [pid=11524] vsize: 82832 Current children cumulated CPU time (s) 499 Current children cumulated vsize (Kb) 84956 [startup+510.058 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20739 0 2 0 50795 105 0 0 25 0 1 0 1851813928 84951040 19258 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20740 19258 145 145 0 20595 0 [pid=11524] vsize: 82960 Current children cumulated CPU time (s) 509.01 Current children cumulated vsize (Kb) 85084 [startup+520.059 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20762 0 2 0 51794 105 0 0 25 0 1 0 1851813928 85049344 19281 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20764 19281 145 145 0 20619 0 [pid=11524] vsize: 83056 Current children cumulated CPU time (s) 519 Current children cumulated vsize (Kb) 85180 [startup+530.061 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20767 0 2 0 52794 106 0 0 25 0 1 0 1851813928 85065728 19286 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20768 19286 145 145 0 20623 0 [pid=11524] vsize: 83072 Current children cumulated CPU time (s) 529.01 Current children cumulated vsize (Kb) 85196 [startup+540.061 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20791 0 2 0 53793 106 0 0 25 0 1 0 1851813928 85164032 19310 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20792 19310 145 145 0 20647 0 [pid=11524] vsize: 83168 Current children cumulated CPU time (s) 539 Current children cumulated vsize (Kb) 85292 [startup+550.063 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20900 0 2 0 54792 107 0 0 25 0 1 0 1851813928 85233664 19328 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20809 19328 145 145 0 20664 0 [pid=11524] vsize: 83236 Current children cumulated CPU time (s) 549 Current children cumulated vsize (Kb) 85360 [startup+560.065 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20976 0 2 0 55791 108 0 0 25 0 1 0 1851813928 85381120 19364 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20845 19364 145 145 0 20700 0 [pid=11524] vsize: 83380 Current children cumulated CPU time (s) 559 Current children cumulated vsize (Kb) 85504 [startup+570.065 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21017 0 2 0 56790 108 0 0 25 0 1 0 1851813928 85336064 19353 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20834 19353 145 145 0 20689 0 [pid=11524] vsize: 83336 Current children cumulated CPU time (s) 568.99 Current children cumulated vsize (Kb) 85460 [startup+580.067 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21035 0 2 0 57790 109 0 0 25 0 1 0 1851813928 85409792 19371 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20852 19371 145 145 0 20707 0 [pid=11524] vsize: 83408 Current children cumulated CPU time (s) 579 Current children cumulated vsize (Kb) 85532 [startup+590.068 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21049 0 2 0 58790 110 0 0 25 0 1 0 1851813928 85463040 19385 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20865 19385 145 145 0 20720 0 [pid=11524] vsize: 83460 Current children cumulated CPU time (s) 589.01 Current children cumulated vsize (Kb) 85584 [startup+600.068 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21082 0 2 0 59789 110 0 0 25 0 1 0 1851813928 85602304 19418 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11524/statm): 20899 19418 145 145 0 20754 0 [pid=11524] vsize: 83596 Current children cumulated CPU time (s) 599 Current children cumulated vsize (Kb) 85720 [startup+610.07 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21115 0 2 0 60788 111 0 0 25 0 1 0 1851813928 85745664 19451 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 20934 19451 145 145 0 20789 0 [pid=11524] vsize: 83736 Current children cumulated CPU time (s) 609 Current children cumulated vsize (Kb) 85860 [startup+620.071 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21136 0 2 0 61788 111 0 0 25 0 1 0 1851813928 85815296 19472 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 20951 19472 145 145 0 20806 0 [pid=11524] vsize: 83804 Current children cumulated CPU time (s) 619 Current children cumulated vsize (Kb) 85928 [startup+630.071 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21155 0 2 0 62788 111 0 0 25 0 1 0 1851813928 85893120 19491 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 20970 19491 145 145 0 20825 0 [pid=11524] vsize: 83880 Current children cumulated CPU time (s) 629 Current children cumulated vsize (Kb) 86004 [startup+640.072 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21169 0 2 0 63788 112 0 0 25 0 1 0 1851813928 85954560 19505 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 20985 19505 145 145 0 20840 0 [pid=11524] vsize: 83940 Current children cumulated CPU time (s) 639.01 Current children cumulated vsize (Kb) 86064 [startup+650.073 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21177 0 2 0 64787 112 0 0 25 0 1 0 1851813928 85983232 19513 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 20992 19513 145 145 0 20847 0 [pid=11524] vsize: 83968 Current children cumulated CPU time (s) 649 Current children cumulated vsize (Kb) 86092 [startup+660.073 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21199 0 2 0 65787 112 0 0 25 0 1 0 1851813928 86089728 19535 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21018 19535 145 145 0 20873 0 [pid=11524] vsize: 84072 Current children cumulated CPU time (s) 659 Current children cumulated vsize (Kb) 86196 [startup+670.074 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21296 0 2 0 66787 112 0 0 25 0 1 0 1851813928 86102016 19541 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21021 19541 145 145 0 20876 0 [pid=11524] vsize: 84084 Current children cumulated CPU time (s) 669 Current children cumulated vsize (Kb) 86208 [startup+680.076 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21310 0 2 0 67787 112 0 0 25 0 1 0 1851813928 86155264 19555 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21034 19555 145 145 0 20889 0 [pid=11524] vsize: 84136 Current children cumulated CPU time (s) 679 Current children cumulated vsize (Kb) 86260 [startup+690.076 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21322 0 2 0 68787 112 0 0 25 0 1 0 1851813928 86200320 19567 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21045 19567 145 145 0 20900 0 [pid=11524] vsize: 84180 Current children cumulated CPU time (s) 689 Current children cumulated vsize (Kb) 86304 [startup+700.078 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21350 0 2 0 69788 112 0 0 25 0 1 0 1851813928 86310912 19595 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21072 19595 145 145 0 20927 0 [pid=11524] vsize: 84288 Current children cumulated CPU time (s) 699.01 Current children cumulated vsize (Kb) 86412 [startup+710.079 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21365 0 2 0 70788 112 0 0 25 0 1 0 1851813928 86376448 19610 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21088 19610 145 145 0 20943 0 [pid=11524] vsize: 84352 Current children cumulated CPU time (s) 709.01 Current children cumulated vsize (Kb) 86476 [startup+720.078 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21442 0 2 0 71787 113 0 0 25 0 1 0 1851813928 86528000 19648 4294967295 134512640 135094434 3221224432 3221220224 134600314 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21125 19648 145 145 0 20980 0 [pid=11524] vsize: 84500 Current children cumulated CPU time (s) 719.01 Current children cumulated vsize (Kb) 86624 [startup+730.079 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21483 0 2 0 72786 114 0 0 25 0 1 0 1851813928 86487040 19638 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21115 19638 145 145 0 20970 0 [pid=11524] vsize: 84460 Current children cumulated CPU time (s) 729.01 Current children cumulated vsize (Kb) 86584 [startup+740.08 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21492 0 2 0 73787 114 0 0 25 0 1 0 1851813928 86519808 19647 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21123 19647 145 145 0 20978 0 [pid=11524] vsize: 84492 Current children cumulated CPU time (s) 739.02 Current children cumulated vsize (Kb) 86616 [startup+750.082 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21504 0 2 0 74787 114 0 0 25 0 1 0 1851813928 86564864 19659 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21134 19659 145 145 0 20989 0 [pid=11524] vsize: 84536 Current children cumulated CPU time (s) 749.02 Current children cumulated vsize (Kb) 86660 [startup+760.082 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21515 0 2 0 75785 115 0 0 25 0 1 0 1851813928 86609920 19670 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21145 19670 145 145 0 21000 0 [pid=11524] vsize: 84580 Current children cumulated CPU time (s) 759.01 Current children cumulated vsize (Kb) 86704 [startup+770.083 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21526 0 2 0 76785 116 0 0 25 0 1 0 1851813928 86654976 19681 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21156 19681 145 145 0 21011 0 [pid=11524] vsize: 84624 Current children cumulated CPU time (s) 769.02 Current children cumulated vsize (Kb) 86748 [startup+780.084 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21543 0 2 0 77785 116 0 0 25 0 1 0 1851813928 86724608 19698 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21173 19698 145 145 0 21028 0 [pid=11524] vsize: 84692 Current children cumulated CPU time (s) 779.02 Current children cumulated vsize (Kb) 86816 [startup+790.084 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21645 0 2 0 78784 117 0 0 25 0 1 0 1851813928 86765568 19709 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21183 19709 145 145 0 21038 0 [pid=11524] vsize: 84732 Current children cumulated CPU time (s) 789.02 Current children cumulated vsize (Kb) 86856 [startup+800.086 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21667 0 2 0 79783 118 0 0 25 0 1 0 1851813928 86855680 19731 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21205 19731 145 145 0 21060 0 [pid=11524] vsize: 84820 Current children cumulated CPU time (s) 799.02 Current children cumulated vsize (Kb) 86944 [startup+810.087 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21680 0 2 0 80784 118 0 0 25 0 1 0 1851813928 86904832 19744 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21217 19744 145 145 0 21072 0 [pid=11524] vsize: 84868 Current children cumulated CPU time (s) 809.03 Current children cumulated vsize (Kb) 86992 [startup+820.087 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21699 0 2 0 81783 118 0 0 25 0 1 0 1851813928 86986752 19763 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21237 19763 145 145 0 21092 0 [pid=11524] vsize: 84948 Current children cumulated CPU time (s) 819.02 Current children cumulated vsize (Kb) 87072 [startup+830.088 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21800 0 2 0 82783 119 0 0 25 0 1 0 1851813928 87011328 19772 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21243 19772 145 145 0 21098 0 [pid=11524] vsize: 84972 Current children cumulated CPU time (s) 829.03 Current children cumulated vsize (Kb) 87096 [startup+840.089 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21891 0 2 0 83781 119 0 0 25 0 1 0 1851813928 87248896 19830 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21301 19830 145 145 0 21156 0 [pid=11524] vsize: 85204 Current children cumulated CPU time (s) 839.01 Current children cumulated vsize (Kb) 87328 [startup+850.089 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21908 0 2 0 84782 119 0 0 25 0 1 0 1851813928 87318528 19847 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19847 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 849.02 Current children cumulated vsize (Kb) 87396 [startup+860.09 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 85782 119 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 859.02 Current children cumulated vsize (Kb) 87396 [startup+870.09 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 86782 120 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 869.03 Current children cumulated vsize (Kb) 87396 [startup+880.091 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 87782 120 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223056 134562142 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 879.03 Current children cumulated vsize (Kb) 87396 [startup+890.091 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 88782 120 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 889.03 Current children cumulated vsize (Kb) 87396 [startup+900.091 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21910 0 2 0 89782 120 0 0 25 0 1 0 1851813928 87318528 19849 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19849 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 899.03 Current children cumulated vsize (Kb) 87396 [startup+910.091 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21910 0 2 0 90782 120 0 0 25 0 1 0 1851813928 87318528 19849 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19849 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 909.03 Current children cumulated vsize (Kb) 87396 [startup+920.092 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21910 0 2 0 91782 120 0 0 25 0 1 0 1851813928 87318528 19849 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21318 19849 145 145 0 21173 0 [pid=11524] vsize: 85272 Current children cumulated CPU time (s) 919.03 Current children cumulated vsize (Kb) 87396 [startup+930.093 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21918 0 2 0 92782 120 0 0 25 0 1 0 1851813928 87351296 19857 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21326 19857 145 145 0 21181 0 [pid=11524] vsize: 85304 Current children cumulated CPU time (s) 929.03 Current children cumulated vsize (Kb) 87428 [startup+940.094 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21935 0 2 0 93782 121 0 0 25 0 1 0 1851813928 87416832 19874 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21342 19874 145 145 0 21197 0 [pid=11524] vsize: 85368 Current children cumulated CPU time (s) 939.04 Current children cumulated vsize (Kb) 87492 [startup+950.094 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21950 0 2 0 94782 121 0 0 25 0 1 0 1851813928 87482368 19889 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21358 19889 145 145 0 21213 0 [pid=11524] vsize: 85432 Current children cumulated CPU time (s) 949.04 Current children cumulated vsize (Kb) 87556 [startup+960.095 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22021 0 2 0 95782 121 0 0 25 0 1 0 1851813928 87609344 19921 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21389 19921 145 145 0 21244 0 [pid=11524] vsize: 85556 Current children cumulated CPU time (s) 959.04 Current children cumulated vsize (Kb) 87680 [startup+970.096 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22054 0 2 0 96781 121 0 0 25 0 1 0 1851813928 87535616 19903 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21371 19903 145 145 0 21226 0 [pid=11524] vsize: 85484 Current children cumulated CPU time (s) 969.03 Current children cumulated vsize (Kb) 87608 [startup+980.097 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22155 0 2 0 97780 122 0 0 25 0 1 0 1851813928 87576576 19913 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21381 19913 145 145 0 21236 0 [pid=11524] vsize: 85524 Current children cumulated CPU time (s) 979.03 Current children cumulated vsize (Kb) 87648 [startup+990.098 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22165 0 2 0 98780 122 0 0 25 0 1 0 1851813928 87613440 19923 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21390 19923 145 145 0 21245 0 [pid=11524] vsize: 85560 Current children cumulated CPU time (s) 989.03 Current children cumulated vsize (Kb) 87684 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22180 0 2 0 99780 122 0 0 25 0 1 0 1851813928 87678976 19938 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21406 19938 145 145 0 21261 0 [pid=11524] vsize: 85624 Current children cumulated CPU time (s) 999.03 Current children cumulated vsize (Kb) 87748 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22194 0 2 0 100780 122 0 0 25 0 1 0 1851813928 87732224 19952 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21419 19952 145 145 0 21274 0 [pid=11524] vsize: 85676 Current children cumulated CPU time (s) 1009.03 Current children cumulated vsize (Kb) 87800 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22209 0 2 0 101780 122 0 0 25 0 1 0 1851813928 87789568 19967 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21433 19967 145 145 0 21288 0 [pid=11524] vsize: 85732 Current children cumulated CPU time (s) 1019.03 Current children cumulated vsize (Kb) 87856 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22222 0 2 0 102780 122 0 0 25 0 1 0 1851813928 87842816 19980 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21446 19980 145 145 0 21301 0 [pid=11524] vsize: 85784 Current children cumulated CPU time (s) 1029.03 Current children cumulated vsize (Kb) 87908 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22236 0 2 0 103780 123 0 0 25 0 1 0 1851813928 87900160 19994 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21460 19994 145 145 0 21315 0 [pid=11524] vsize: 85840 Current children cumulated CPU time (s) 1039.04 Current children cumulated vsize (Kb) 87964 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22251 0 2 0 104780 123 0 0 25 0 1 0 1851813928 87961600 20009 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21475 20009 145 145 0 21330 0 [pid=11524] vsize: 85900 Current children cumulated CPU time (s) 1049.04 Current children cumulated vsize (Kb) 88024 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22295 0 2 0 105780 123 0 0 25 0 1 0 1851813928 88272896 20053 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21551 20053 145 145 0 21406 0 [pid=11524] vsize: 86204 Current children cumulated CPU time (s) 1059.04 Current children cumulated vsize (Kb) 88328 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22295 0 2 0 106781 123 0 0 25 0 1 0 1851813928 88272896 20053 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21551 20053 145 145 0 21406 0 [pid=11524] vsize: 86204 Current children cumulated CPU time (s) 1069.05 Current children cumulated vsize (Kb) 88328 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22295 0 2 0 107781 123 0 0 25 0 1 0 1851813928 88272896 20053 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21551 20053 145 145 0 21406 0 [pid=11524] vsize: 86204 Current children cumulated CPU time (s) 1079.05 Current children cumulated vsize (Kb) 88328 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22300 0 2 0 108781 123 0 0 25 0 1 0 1851813928 88289280 20058 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21555 20058 145 145 0 21410 0 [pid=11524] vsize: 86220 Current children cumulated CPU time (s) 1089.05 Current children cumulated vsize (Kb) 88344 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 11524 Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11520/statm): 531 226 485 147 0 384 0 [pid=11520] vsize: 2124 Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22315 0 2 0 109781 123 0 0 25 0 1 0 1851813928 88346624 20073 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11524/statm): 21569 20073 145 145 0 21424 0 [pid=11524] vsize: 86276 Current children cumulated CPU time (s) 1099.05 Current children cumulated vsize (Kb) 88400 One traced child (pid=11524) exited with status: 30 One traced child (pid=11520) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 1109.69 CPU time (s): 1108.66 CPU user time (s): 1107.36 CPU system time (s): 1.3028 CPU usage (%): 99.9071 Max. virtual memory (cumulated for all children) (Kb): 88400
Verifier: OK 471047168