PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-egout.opb
MD5SUM	9f6abccf92594d7ee18b1409c45097d3
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	471047168
Optimality of the best value was proved	NO
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	SAT
Best CPU time to get the best result obtained on this benchmark	1098.43
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
Trace number 30696

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-05-25 18:40:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22092 boxname=wulflinc18 idbench=908 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  9f6abccf92594d7ee18b1409c45097d3  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-egout.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-egout.opb
IDLAUNCH: 22092
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        734168 kB
Buffers:         38540 kB
Cached:         233892 kB
SwapCached:        588 kB
Active:          70732 kB
Inactive:       207084 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        733916 kB
SwapTotal:     2097892 kB
SwapFree:      2096632 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            17072 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 18:58:43 (client local time) WITH STATUS 30 IN 1098.43 SECONDS
stats: 22092 0 1098.43 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
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         (124 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1097.58 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.77 0.94 0.97 2/54 4850
Raw data (stat): 4850 (runsolver) R 4849 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841098435 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99988 s]
Raw data (loadavg): 0.81 0.94 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0014 s]
Raw data (loadavg): 0.84 0.94 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0022 s]
Raw data (loadavg): 0.86 0.94 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0018 s]
Raw data (loadavg): 0.88 0.94 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0031 s]
Raw data (loadavg): 0.90 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0107 s]
Raw data (loadavg): 0.91 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.1145 s]
Raw data (loadavg): 0.93 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.1159 s]
Raw data (loadavg): 0.94 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.1158 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.116 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.118 s]
Raw data (loadavg): 0.96 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.12 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.12 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.12 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.121 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.122 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.123 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.124 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.124 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.125 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.125 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.125 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.126 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.126 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.126 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.127 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.128 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.129 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.13 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.131 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.132 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.133 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.134 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.133 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.135 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.136 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.136 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.136 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.136 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.137 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.137 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.138 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.138 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.139 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.14 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.139 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.14 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.141 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.14 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.141 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.141 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.142 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.142 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.142 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.142 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.143 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.144 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.143 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.143 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.145 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.145 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.146 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.146 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.147 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.147 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.147 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.148 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.149 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.149 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.149 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.15 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.151 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.151 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.151 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.152 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.152 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.153 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.154 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.154 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.154 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.154 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.154 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.154 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.155 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.155 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.155 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.156 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.156 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.156 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.157 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.158 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.159 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.16 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.159 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.159 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.161 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.161 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.161 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.161 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.16 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.16 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.16 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.16 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.17 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.17 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.17 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.17 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.17 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.17 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1098.34 s]
Raw data (loadavg): 0.99 0.97 0.97 1/53 4854
Raw data (stat): 4850 (minisat+_script) S 4849 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841098435 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 1098.34
CPU time (s): 1098.43
CPU user time (s): 1097.67
CPU system time (s): 0.760884
CPU usage (%): 100.008
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	471047168
#### END VERIFIER DATA ####