#!/usr/bin/env python3 """check_c71_n18.py -- self-contained verifier for a new C_71 (FEI) lower bound. C_71 >= 6.5218457109230465756581439729485784683666 (n=18 explicit balanced logic-monotone function; headline 18-digit floor truncation: 6.521845710923046575) Standalone: Python 3.9+ and mpmath only; zero repository imports. Same template as the MI2026b n=17 verifier (check_c71_n17.py, DOI 10.5281/zenodo.21113935); the certificate truth table is inlined below and bound by its SHA-256. CONSTRUCTION (one sentence): the MI2026b n=17 record function, with the four inputs on which tail variable x_10 acts split two-and-two between x_10 and the new 18th variable -- equalising every auxiliary variable's action at exactly two cells of the 9-variable majority core (uniform hosting), which raises the spectral entropy by exactly twice the moved weight at identical total influence 261/128; the certified gain over the n=17 record is exactly 1/133. CONVENTION (matches constants/71a.md, ODWZ 2011, Hod arXiv:1711.00762): * f : {-1,+1}^n -> {-1,+1}; TRUE = -1 (Hod). Truth-table encoding: index x in [0, 2^n); bit i of x set <=> x_{i+1} = -1 = TRUE. * fhat(S) = E_x[f(x) chi_S(x)], uniform measure; integer WHT gives a_S = 2^n fhat(S); weights w_S = a_S^2/4^n exact Fractions. * H = sum over ALL S (incl. emptyset) of w_S log2(1/w_S). LOG BASE 2. * I = sum_S w_S |S| (= average sensitivity), exact Fraction. * Parseval sum w_S == 1 asserted; all verdicts are exact rational comparisons of interval endpoints. No float enters any decision. * SHA-256 binding: sha256 of the comma-joined decimal truth table ("1,-1,...") must equal the certificate's truth_table_sha256. * Amplification: O'Donnell-Tan 2013 / Hod 2017 Prop 1.2 -- g balanced (fhat(0)=0 exactly), H[g] > 0, then C_71 >= H[g]/(I[g]-1). Both hypotheses are verified below, never assumed. * The bar is the PREVIOUS record's certified UPPER endpoint 6.514326913930565372650625175957 (MI2026b), so the strict improvement is itself certified, not merely implied by truncations. USAGE: python3 check_c71_n18.py [--dps N] # selftest + the certificate python3 check_c71_n18.py --selftest # anchors only Exit 0 iff the selftest passes and the bound is CERTIFIED. """ import hashlib import sys from fractions import Fraction import mpmath from mpmath import iv # previous record: MI2026b certified interval upper endpoint (strict bar) RECORD = Fraction(6514326913930565372650625175957, 10**30) RECORD_STR = "6.514326913930565372650625175957" CERTS = [ { "name": "n=18 terminal (headline record, logic-monotone)", "n": 18, "truth_table_true_hex": ( "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc88feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000" "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00" "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000" ), "truth_table_sha256": "f8a7bb2c738d86368305111633376b1a3a83d8ee1f1abcc9a37d841b0f9c7839", "claimed_I": "261/128", "monotone": True, "claimed_value_prefix": "6.5218457109230465756581439729485784683666", }, ] # ------------------------------------------------------------------ exact core def wht(table): a = list(table) h = 1 while h < len(a): for i in range(0, len(a), 2 * h): for j in range(i, i + h): x, y = a[j], a[j + h] a[j], a[j + h] = x + y, x - y h *= 2 return a def spectrum(table): N = len(table) a = wht(table) w = {s: Fraction(c * c, N * N) for s, c in enumerate(a) if c != 0} assert sum(w.values()) == 1, "Parseval failed: sum w_S != 1" return w, a[0] def influence(weights): return sum(wS * bin(s).count("1") for s, wS in weights.items()) def table_from_hex(n, true_hex): mask = int(true_hex, 16) assert mask < (1 << (1 << n)) return [-1 if (mask >> x) & 1 else 1 for x in range(1 << n)] def is_logic_monotone(table, n): for i in range(n): b = 1 << i for x in range(1 << n): if not x & b and table[x] == -1 and table[x | b] == +1: return False return True # ------------------------------------------------------------ interval helpers def iv_frac(q): return iv.mpf(int(q.numerator)) / iv.mpf(int(q.denominator)) def endpoint_frac(raw): sign, man, exp, _ = raw if man == 0: return Fraction(0) v = Fraction(man) * (Fraction(2) ** exp) return -v if sign else v def entropy_interval(weights): counts = {} for wS in weights.values(): counts[wS] = counts.get(wS, 0) + 1 H = iv.mpf(0) ln2 = iv.log(2) for wS, m in counts.items(): if wS == 1: continue H += (iv.mpf(m) * iv_frac(wS) * (iv.log(int(wS.denominator)) - iv.log(int(wS.numerator))) / ln2) return H def h_interval(q): if q == 0 or q == 1: return iv.mpf(0) return entropy_interval({0: q, 1: 1 - q}) # -------------------------------------------------------------- the certificate def check_cert(cert): n = cert["n"] table = table_from_hex(n, cert["truth_table_true_hex"]) sha = hashlib.sha256(",".join(str(v) for v in table).encode()).hexdigest() assert sha == cert["truth_table_sha256"], "sha256 binding to cert FAILS" if cert["monotone"]: assert is_logic_monotone(table, n), "monotone claim FAILS" weights, a0 = spectrum(table) I = influence(weights) assert I == Fraction(cert["claimed_I"]), f"I mismatch: computed {I}" assert a0 == 0, "amplified ratio requires a balanced function (fhat(0)=0)" assert I > 1, "amplified ratio requires I > 1" H = entropy_interval(weights) ratio = H / iv_frac(I - 1) lo, hi = endpoint_frac(ratio._mpi_[0]), endpoint_frac(ratio._mpi_[1]) assert endpoint_frac(H._mpi_[0]) > 0, "H > 0 hypothesis" claimed = Fraction(*_dec(cert["claimed_value_prefix"])) ok = (lo > RECORD) and (claimed <= lo) print(f"{cert['name']}: n={n}, balanced (fhat(0)=0): True, I = {I}, " f"monotone = {cert['monotone']}, sha256 binding OK, " f"{len(weights)} nonzero coefficients") print(f" C = H/(I-1) certified in [{_floor(lo, 30)}..., {_ceil(hi, 30)}...]") print(f" claimed (floor-truncated) {cert['claimed_value_prefix']}") print(f" headline (18-digit floor of lower endpoint) {_floor(lo, 18)}") print(f" claimed <= lower endpoint: {claimed <= lo}; " f"lower endpoint > {RECORD_STR} (prev record certified hi): {lo > RECORD}") print(" CERTIFIED" if ok else " NOT CERTIFIED") return ok def _dec(s): a, b = s.split(".") return int(a + b), 10 ** len(b) def _floor(fr, k): sc = fr * 10 ** k s = str(sc.numerator // sc.denominator).rjust(k + 1, "0") return s[:-k] + "." + s[-k:] def _ceil(fr, k): sc = fr * 10 ** k s = str(-((-sc.numerator) // sc.denominator)).rjust(k + 1, "0") return s[:-k] + "." + s[-k:] # ------------------------------------------------------------------- selftest def beta_half_interval(K=220): """Hod Thm 4.4 anchor beta(1/2): exact q-ladder, interval h, certified tail.""" z = Fraction(1, 2) qs = [z] for _ in range(K + 2): qs.append(1 / (1 + qs[-1])) S = h_interval(qs[0]) / iv_frac(1 - z) + h_interval(qs[1]) / iv_frac(z) pi = Fraction(1) for k in range(0, K + 1): if k >= 1: pi *= qs[k] S += h_interval(qs[k + 2]) * iv_frac(pi) r = max(qs[K + 1], qs[K + 2]) S += iv_frac(pi * r / (1 - r)) * iv.mpf([0, 1]) return S def selftest(): failures = [] maj3 = [-1 if bin(x).count("1") >= 2 else 1 for x in range(8)] w, a0 = spectrum(maj3) H = entropy_interval(w) ok = (a0 == 0 and influence(w) == Fraction(3, 2) and endpoint_frac(H._mpi_[0]) <= 2 <= endpoint_frac(H._mpi_[1])) print(f"selftest Maj3: I = {influence(w)} (want 3/2), H brackets 2: " f"{'PASS' if ok else 'FAIL'}") if not ok: failures.append("Maj3") b = beta_half_interval() blo, bhi = endpoint_frac(b._mpi_[0]), endpoint_frac(b._mpi_[1]) ok = (Fraction(645478371656, 10**11) < blo <= bhi < Fraction(645478371657, 10**11) and bhi < RECORD) print(f"selftest beta(1/2) in [{_floor(blo, 12)}, {_ceil(bhi, 12)}] " f"(want 6.45478371656..., < prev record): {'PASS' if ok else 'FAIL'}") if not ok: failures.append("beta(1/2)") print("SELFTEST", "PASS" if not failures else f"FAIL: {failures}") return not failures def main(argv): dps = 120 if "--dps" in argv: i = argv.index("--dps") dps = int(argv[i + 1]) iv.dps = dps mpmath.mp.dps = dps ok = selftest() if "--selftest" in argv: return 0 if ok else 1 for cert in CERTS: ok = check_cert(cert) and ok print("ALL CERTIFIED" if ok else "FAILURE") return 0 if ok else 1 if __name__ == "__main__": sys.exit(main(sys.argv[1:]))