pxfm 0.1.29

/*
 * // Copyright (c) Radzivon Bartoshyk 8/2025. All rights reserved.
 * //
 * // Redistribution and use in source and binary forms, with or without modification,
 * // are permitted provided that the following conditions are met:
 * //
 * // 1.  Redistributions of source code must retain the above copyright notice, this
 * // list of conditions and the following disclaimer.
 * //
 * // 2.  Redistributions in binary form must reproduce the above copyright notice,
 * // this list of conditions and the following disclaimer in the documentation
 * // and/or other materials provided with the distribution.
 * //
 * // 3.  Neither the name of the copyright holder nor the names of its
 * // contributors may be used to endorse or promote products derived from
 * // this software without specific prior written permission.
 * //
 * // THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * // AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * // IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * // DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * // FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * // DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * // SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * // CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * // OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * // OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */

/**
Poly for x/erf(x) generated by Sollya and SageMath:
```python
def build_sollya_script(idx):
    return f"""
d = [{idx}/16, {idx + 1}/16];

f = x/erf(x);
Q = fpminimax(f, [|0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20|], [|107...|], d);

for i from 0 to degree(Q) by 2 do {{
    write(coeff(Q, i)) >> "coefficients.txt";
    write("\\n") >> "coefficients.txt";
}};
"""

def load_coefficients(filename):
    with open(filename, "r") as f:
        return [RealField(500)(line.strip()) for line in f if line.strip()]

def call_sollya_on_interval(idx):
    sollya_script = build_sollya_script(idx)
    with open("tmp_interval.sollya", "w") as f:
        f.write(sollya_script)
    import subprocess
    if os.path.exists("coefficients.txt"):
        os.remove("coefficients.txt")
    try:
        result = subprocess.run(
            ["sollya", "tmp_interval.sollya"],
            check=True,
            capture_output=True,
            text=True
        )
    except subprocess.CalledProcessError as e:
        return

def print_coeffs(poly):
    print("[")
    for i in range(len(poly)):
        coeff = poly[i]
        print_double_double("", coeff)
    print("],")

print(f"pub(crate) static RERF_HARD: [[(u64, u64); 11]; 96] = [")
for i in range(0, 96):
    call_sollya_on_interval(i)
    coeffs = load_coefficients(f"coefficients.txt")
    print_coeffs(coeffs)
print("];")
```
**/
pub(crate) static RERF_HARD: [[(u64, u64); 11]; 96] = [
    [
        (0xbc8618f13eb7ca89, 0x3fec5bf891b4ef6b),
        (0xbc6d7696fe4a8276, 0x3fd2e7fb0bcdf4f2),
        (0xbc0cb8b8ee1a9698, 0x3f842aa561ecc102),
        (0x3c1cd7ccb69e95dd, 0xbf75207c7ef80727),
        (0xbbaa394a1107572c, 0x3f2db4a8d7c32477),
        (0x3b947772cadb5350, 0x3f20faa7a99a39f6),
        (0x3b82456978771f64, 0xbef3adb844cdd880),
        (0x3b37f7e102aeadc8, 0xbec366744e62af3d),
        (0xbb4abc03ab72db68, 0x3eaaf1daea64176d),
        (0xbb198547c9f8a468, 0xbeab1e39a7a0e2e7),
        (0x3b7f74a4a9ee36d8, 0x3f04a9e81d9c80b1),
    ],
    [
        (0xbc8618f13eb7ca80, 0x3fec5bf891b4ef6b),
        (0xbc6d7696fe4b2b7e, 0x3fd2e7fb0bcdf4f2),
        (0xbc0cb8b91c2650c4, 0x3f842aa561ecc102),
        (0x3c1cdab546730682, 0xbf75207c7ef80727),
        (0x3bbb63455d753552, 0x3f2db4a8d7c3246e),
        (0xbbb424fd3813a0d0, 0x3f20faa7a99a56cc),
        (0xbb974ceb097ab454, 0xbef3adb846a857a7),
        (0x3b61d21be7b25ec5, 0xbec3666116b38c11),
        (0x3b3682e9db421864, 0x3eaab4cd09f0d085),
        (0x3aa5c983c010eade, 0x3e03700f5101836c),
        (0xbae41b274c7a5708, 0xbe5a9d21ba05e7ff),
    ],
    [
        (0xbc8618f13eace57e, 0x3fec5bf891b4ef6b),
        (0xbc6d76974e25c204, 0x3fd2e7fb0bcdf4f2),
        (0xbc0ca83c7b5744b0, 0x3f842aa561ecc102),
        (0x3c18ce0252a1d68a, 0xbf75207c7ef80727),
        (0x3bce42420bd5d0b7, 0x3f2db4a8d7c32516),
        (0xbbb957874ae4a150, 0x3f20faa7a99a30ee),
        (0x3b8ddca7ef22dfae, 0xbef3adb8467833bb),
        (0xbb651d1f2d5b7a26, 0xbec3666141b05fd7),
        (0x3aeee8bd696a7e40, 0x3eaab4da0fa3f61f),
        (0xbaaea92dba36c4b8, 0x3e00fecb2644094c),
        (0x3ac784c24cdd6540, 0xbe5a2dbb95d32849),
    ],
    [
        (0xbc8618f0f4f60562, 0x3fec5bf891b4ef6b),
        (0xbc6d77a534ca7ed6, 0x3fd2e7fb0bcdf4f2),
        (0xbbb70f4c473c9e00, 0x3f842aa561ecc102),
        (0xbc1a977c9db0b237, 0xbf75207c7ef80734),
        (0xbbc2d4a01ff162d0, 0x3f2db4a8d7c36d59),
        (0x3b9b8c9eea11c018, 0x3f20faa7a991fd98),
        (0xbb9b38ca273e4e60, 0xbef3adb841391777),
        (0xbb4cea6e9e663e28, 0xbec36663999cb0ce),
        (0x3b2c61386dab24b4, 0x3eaab533e624d8da),
        (0xba652f7751c8cde8, 0x3df1a4ff38724196),
        (0x3af4e3db417be62c, 0xbe597d9d709c8e08),
    ],
    [
        (0xbc8618a3e2026a77, 0x3fec5bf891b4ef6b),
        (0xbc6e20944e2ac138, 0x3fd2e7fb0bcdf4f2),
        (0x3c2e12ce437042e0, 0x3f842aa561ecc10c),
        (0x3c12502cccbcf6b0, 0xbf75207c7ef80a4e),
        (0xbbcb4f065498051c, 0x3f2db4a8d7cd2219),
        (0x3bbf4b458bdec052, 0x3f20faa7a8e99ec9),
        (0x3b961dfc4148cd3a, 0xbef3adb801226409),
        (0x3b5a733630a550c8, 0xbec366748a484948),
        (0xbb4a24fac279758a, 0x3eaab6b15bf3135e),
        (0xba3e1e7b6682ff00, 0xbdf6bd63ad5e418d),
        (0xbafc10a24873a1e6, 0xbe5883474fe6d074),
    ],
    [
        (0xbc85fe3dd629df7a, 0x3fec5bf891b4ef6b),
        (0x3c7db7a5dd1476d1, 0x3fd2e7fb0bcdf4f1),
        (0xbc2f10bd47f8beb3, 0x3f842aa561ecc2a2),
        (0xbc171085831fc822, 0xbf75207c7ef859cf),
        (0xbbad645d9fde8344, 0x3f2db4a8d8721804),
        (0x3bb7d0c1a80cb912, 0x3f20faa7a1860459),
        (0x3b8144a625fe24f0, 0xbef3adb626814084),
        (0xbb6d54a39e361631, 0xbec366c6f18511c4),
        (0x3b418b036802bd18, 0x3eaabb6edc1c9627),
        (0xbaa73c33c857a12e, 0xbe1a953fd40d7420),
        (0x3ad8027476e07af0, 0xbe573402996dd2c2),
    ],
    [
        (0xbc81b66a7b5ccff1, 0x3fec5bf891b4ef6b),
        (0xbc79bd60b5b426c0, 0x3fd2e7fb0bcdf4e9),
        (0xbc0a204cd030c544, 0x3f842aa561ece3d6),
        (0xbbe49cde86af7e88, 0xbf75207c7efcfa9b),
        (0x3bb2554e3ad0acc8, 0x3f2db4a8df415e4a),
        (0x3bae907c3c53747c, 0x3f20faa76a3ce3dd),
        (0x3b576ef184d414a0, 0xbef3adac5933f5ab),
        (0xbb56367067dc7e24, 0xbec367fa0f7f75b1),
        (0xbb3995c8812c5cd2, 0x3eaac7daac27d5c7),
        (0x3acb5505cddd0ffc, 0xbe303e14c38cf6a0),
        (0xbafad790a7b16c40, 0xbe5585acf166b0ba),
    ],
    [
        (0x3c85d1c9c211e918, 0x3fec5bf891b4ef6c),
        (0x3c7dc0f172d28f0b, 0x3fd2e7fb0bcdf448),
        (0xbc2cd8e027009eae, 0x3f842aa561eea354),
        (0xbc086a077cc659f6, 0xbf75207c7f2b7b51),
        (0x3bc0b8cda4fe6154, 0x3f2db4a91237a04d),
        (0x3ba9afd26de84c3c, 0x3f20faa63672fc62),
        (0x3b7fbd4c6465a488, 0xbef3ad83cf5114fe),
        (0x3b6a7dda1ef6dceb, 0xbec36ba8282105aa),
        (0xbb32111eb49ac7ac, 0x3eaae41105399da2),
        (0x3add98a71b27ea8a, 0xbe402d0a88af1d02),
        (0x3ae0a91f20394204, 0xbe5370d92bcc2a46),
    ],
    [
        (0x3c803817d1372452, 0x3fec5bf891b4ef86),
        (0xbc50267f5364549c, 0x3fd2e7fb0bcdec86),
        (0xbc09a8c6f2bdfb78, 0x3f842aa561ff6c1f),
        (0xbc1481492e0d9a28, 0xbf75207c8084dac4),
        (0x3bcd3db423b0d83b, 0x3f2db4aa36bdbd16),
        (0xbbacf5bc5b2c622c, 0x3f20faa0e2396b76),
        (0x3b9659a867f69cff, 0xbef3acf933a983ac),
        (0x3b51d6f1b465e7fe, 0xbec3755a4ed1ff4c),
        (0xbaf686c63e3ebca0, 0x3eab1d46ecad9463),
        (0x3ad9001d67537478, 0xbe4cbb6369bcf991),
        (0xbac3dba508ae78c8, 0xbe50f32dbe9334db),
    ],
    [
        (0x3c7e25fe9d726860, 0x3fec5bf891b4f0b1),
        (0xbc7ab06652d76f68, 0x3fd2e7fb0bcda52f),
        (0xbc279366f3014478, 0x3f842aa5627a5113),
        (0x3c191084f4962937, 0xbf75207c8861bf8f),
        (0x3bcc7278fec26fd4, 0x3f2db4af82fa6c34),
        (0x3b607855cfa9f9c0, 0x3f20fa8d3e0a083b),
        (0xbb9ad1bff06c0295, 0xbef3ab635e1ce916),
        (0xbb52ac297a882c52, 0xbec38be316fa087e),
        (0x3b3566206093fe92, 0x3eab86bb787edab1),
        (0x3ad927375753f59c, 0xbe57893e809642e0),
        (0x3adec7fd7dac2bae, 0xbe4c238076f40165),
    ],
    [
        (0xbc7450f4e5a34d6a, 0x3fec5bf891b4faf9),
        (0x3c6070254f6c97c2, 0x3fd2e7fb0bcba54d),
        (0x3c1f8f97820f81aa, 0x3f842aa56548d807),
        (0x3bc2d77ef02fd540, 0xbf75207cadd38a6f),
        (0x3bc008d39e65c4c1, 0x3f2db4c40d23ef77),
        (0x3bcdc5ae5472cba9, 0x3f20fa4f4740e11c),
        (0xbb75e14939f85e6c, 0xbef3a7522154b882),
        (0xbb60f6b3a1eb8a9a, 0xbec3bae123763846),
        (0x3b491b16febd3218, 0x3eac395e796a3137),
        (0xbb0bab30884bdbf8, 0xbe6212bc42b9a2e0),
        (0xbab8eccd2fe224e0, 0xbe45b61fe119ad92),
    ],
    [
        (0x3c76cf1bebd8f6be, 0x3fec5bf891b542d1),
        (0xbc733582099fcc3e, 0x3fd2e7fb0bc009ee),
        (0x3c0b172518bbd9b8, 0x3f842aa572cff422),
        (0x3bdd3ab1da49a7e0, 0xbf75207d439ef930),
        (0xbbbf954393296a6c, 0x3f2db5083a0025ae),
        (0xbbc233ee942ade70, 0x3f20f9a4b3181e2c),
        (0xbb9431141736d564, 0xbef39e09cd205f73),
        (0x3b5c0416708c428a, 0xbec413c0641365e8),
        (0x3b311ec7c02434ac, 0x3ead513298bd2dd3),
        (0xbb0076afa010fc38, 0xbe6a400d6bbe9756),
        (0x3ab039de17d27b28, 0xbe3da0ada3cb2927),
    ],
    [
        (0xbc80961ba80fa981, 0x3fec5bf891b6dccf),
        (0xbc27d2093e9c3580, 0x3fd2e7fb0b8828f0),
        (0xbc1b60797c0d2948, 0x3f842aa5a9bda8d4),
        (0x3c08a71b89c8f1ae, 0xbf75207f44782913),
        (0x3bbc75fe3c50b94c, 0x3f2db5ccf9b43f81),
        (0xbba70122edae31f0, 0x3f20f805df1b6c19),
        (0x3b92da280ec6be23, 0xbef38b05a18fa724),
        (0x3b6e03aa9603e78a, 0xbec4ad11ca8a9f23),
        (0xbb207645aa426dd4, 0x3eaee794c191d1e9),
        (0xbb1277f7834b907b, 0xbe721f2390f45efb),
        (0xbac2bab97552f26b, 0xbe2ee44166bd4092),
    ],
    [
        (0xbc86412a39a97d22, 0x3fec5bf891be76b4),
        (0x3c6bce7a45dd0c50, 0x3fd2e7fb0aa56f36),
        (0x3c2557e7253abfae, 0x3f842aa6683a6171),
        (0x3c1559b4aafa5f9c, 0xbf7520853439abe3),
        (0xbb931b56d2d59ec0, 0x3f2db7bf11a6dcfd),
        (0x3bb30078186be24c, 0x3f20f484e99876bd),
        (0xbb94ca3a5181c4ee, 0xbef367e9a00dd18a),
        (0x3b622de077c887c0, 0xbec59eb568b2aedc),
        (0x3b5b0c17a3645969, 0x3eb08516c078c57d),
        (0x3b0b158910694e5a, 0xbe77daf6997136dd),
        (0xba909415002bf356, 0xbdf90b2f8adaf43d),
    ],
    [
        (0x3c8eebcc5fdc47b3, 0x3fec5bf891dcc345),
        (0xbc7bdeb76ca780cf, 0x3fd2e7fb0797f73d),
        (0x3c10bf8295c1d6f2, 0x3f842aa89fda59cf),
        (0x3bf71f4b638009f4, 0xbf7520947eb352dd),
        (0x3bc81c2b39c7cfa7, 0x3f2dbc13cf992042),
        (0xbbcd2ae351951d22, 0x3f20edc7c5c2c729),
        (0x3b715d146b0c26a8, 0xbef32d944e41faf6),
        (0xbb6803167e74aae4, 0xbec6f973a7c3b9d4),
        (0xbb5698b55b8efe74, 0x3eb1d7b8c937b349),
        (0x3b1b643c9a997ac0, 0xbe7dfd096f4a5fa7),
        (0xba8fb6dd2d7a7030, 0x3e267fb86eba06c2),
    ],
    [
        (0x3c86dc4ce01692a8, 0x3fec5bf892422403),
        (0x3c6e1211450bce0e, 0x3fd2e7fafeac6014),
        (0xbbfac1ba719423a8, 0x3f842aae4848982d),
        (0x3bf7686d089e7c08, 0xbf7520b68fd53c70),
        (0xbbbfc998753b244c, 0x3f2dc4802e8aeb22),
        (0xbba4c102da8c2be4, 0x3f20e25750bd0372),
        (0xbb62a950af6d7a38, 0xbef2d72aa1889a4a),
        (0xbb5d08f83a362a90, 0xbec8b99e783f6f6c),
        (0xbb5a15ec3de1bc4b, 0x3eb35589957ab913),
        (0x3b238126ff764adf, 0xbe8202891efeec09),
        (0xbace98afae47d9fe, 0x3e363d29bdcd0d91),
    ],
    [
        (0x3c87e39a19b3d0c6, 0x3fec5bf89359d0b8),
        (0xbc74ed6ab85ab940, 0x3fd2e7fae8fcf8a7),
        (0x3c236cc1abf3c943, 0x3f842aba66ba4606),
        (0xbc175eb282d39023, 0xbf7520f6d89f5b09),
        (0x3bc0d4196881a655, 0x3f2dd28079e0bef9),
        (0x3bc21692d4ce8e46, 0x3f20d1982ee796d5),
        (0x3b677efb5a2869f0, 0xbef267c3cd8ec55d),
        (0x3b61b3a6e7d66719, 0xbecab655d18fe460),
        (0xbb5c2fcc91af77b1, 0x3eb4d3150ddbaa9c),
        (0x3b23a75514e0479a, 0xbe84a998a5fc1c26),
        (0x3ad030148c0b6a26, 0x3e3ebef94909972c),
    ],
    [
        (0xbc885896855a57a0, 0x3fec5bf895afed62),
        (0xbc7f2cb90899316b, 0x3fd2e7fabfc54d4d),
        (0xbc1101eb755b3912, 0x3f842acedf24073a),
        (0x3c1d800e32be466e, 0xbf75215754e511d7),
        (0xbbbd7331487b23d4, 0x3f2de52c38f47908),
        (0x3bc0f459fff1ce70, 0x3f20bdc1658e0283),
        (0xbb3e9c5de054df00, 0xbef1f28a151cbecb),
        (0x3b646ea1f49d631e, 0xbecc91c3df6254c0),
        (0x3b3f922df375d0bc, 0x3eb60fbb57ac269e),
        (0xbb2adf22ce6fd8d8, 0xbe869dfb539fe8e7),
        (0x3ae7ff8ad5344063, 0x3e4227d4022456f1),
    ],
    [
        (0xbc8ae090bfd1cee8, 0x3fec5bf898aa52a7),
        (0x3c62380fa44cbb08, 0x3fd2e7fa9085783d),
        (0xbc2bb2a4c308cd8c, 0x3f842ae3f8e02952),
        (0xbc1a80c30380f9a9, 0xbf7521b0bf608ac3),
        (0xbbcc1f24fab1d546, 0x3f2df4b9f3f226b4),
        (0xbbbe2b985bc87e80, 0x3f20aee6ee37d5fe),
        (0xbb956ef789bc02ec, 0xbef1a3ac85b7c6fa),
        (0x3b64f04fb6389bef, 0xbecdb12073729082),
        (0xbb5c530a33a8d714, 0x3eb6bba58e548b6b),
        (0xbb28aa08bba90045, 0xbe8791f4b89ddd8a),
        (0x3add8797a6eed87e, 0x3e435face41bc747),
    ],
    [
        (0x3c76800e5118cba2, 0x3fec5bf8955c5890),
        (0xbc66b79aa48d850a, 0x3fd2e7fabdaeecb1),
        (0xbc1d060b60882aea, 0x3f842ad29f1d0d93),
        (0xbc0b7f7e1852d7de, 0xbf75217193e7b656),
        (0xbbb1dfda43c4090c, 0x3f2deb4c771372b5),
        (0x3bc2e3b7bf2030ec, 0x3f20b69da01bfa8a),
        (0xbb74d03bd81ad920, 0xbef1c6b6437d4791),
        (0x3b578508c016669e, 0xbecd44137495d835),
        (0x3b33cb45437e37c4, 0x3eb68402b52f1038),
        (0x3b1be6ce572b06ec, 0xbe874ebcad44d73b),
        (0x3ab4e75545af6170, 0x3e4316a8f4237932),
    ],
    [
        (0x3c8936981c457407, 0x3fec5bf86fa67e7e),
        (0x3c5d1fc5562f5e74, 0x3fd2e7fc9a6db835),
        (0x3c2f4b2630af6de9, 0x3f842a290204d06b),
        (0x3c1a6b67044328aa, 0xbf751f35151a87ad),
        (0x3bca01fb3f4b9119, 0x3f2d9bfe8abb12df),
        (0x3ba530023186fc68, 0x3f20f2eaaebdb0aa),
        (0xbb85c5b20b084330, 0xbef2c599ff9e90f6),
        (0x3b6259424427f91e, 0xbeca60d00700323e),
        (0xbb529d2845b8c334, 0x3eb52404388a56a8),
        (0xbaf9bbc47316c558, 0xbe85c134d3d72756),
        (0xbae4bd922e473c2e, 0x3e418254e80c1fe1),
    ],
    [
        (0x3c77b49c8708d95e, 0x3fec5bf7d439ccf3),
        (0xbc695b6d321a65b0, 0x3fd2e803977ec913),
        (0xbc2b99b73f650bb7, 0x3f8427e578b0c50f),
        (0xbbba4050af501080, 0xbf7518400f97e451),
        (0x3bc8b775372d0f1d, 0x3f2cbb5d411da776),
        (0x3bc0be4772912425, 0x3f218e6db0bf59c7),
        (0x3b777ca8e20895b4, 0xbef51c15be0f3a57),
        (0xbb6e2f3c48e85db8, 0xbec434774a0a089a),
        (0xbb3c765ffe5eadec, 0x3eb276f3778acc12),
        (0xbb0e4efe64d76c5c, 0xbe8300d68f0489e4),
        (0xbac93f2262acf544, 0x3e3dec41980b63a9),
    ],
    [
        (0xbc8e50b3604c6456, 0x3fec5bf5f9905958),
        (0x3c73af2096783c36, 0x3fd2e8171399b082),
        (0x3c26b66b5099742e, 0x3f8422226134cb30),
        (0xbbf2cecc14e6c1fc, 0xbf750815c60e91f8),
        (0x3bcdb6c9be6c6293, 0x3f2adeea8a272502),
        (0xbbb73d5d9ccadd56, 0x3f22bb838b4d286e),
        (0x3b7ab2b233005e94, 0xbef93dba1ccdcc99),
        (0xbb298d7a22372b18, 0xbeb47ed03a750fd0),
        (0xbb3c07e8e0e06602, 0x3ead0ce153b552f1),
        (0x3b00cfb58d5874fc, 0xbe7e9cfd756ceaaf),
        (0x3abaa30adaab76ec, 0x3e37acea6cf7ffff),
    ],
    [
        (0x3c30ec78f45292a0, 0x3fec5bf143d22204),
        (0xbc65249f97c5b9fc, 0x3fd2e8446c72543a),
        (0x3c201cc14aa2fa0b, 0x3f8415d93f136226),
        (0x3c0b56c2e9770fae, 0xbf74e8827285303e),
        (0xbbb6e48066484c1c, 0x3f278a5f412a35b2),
        (0xbbbbbb0c95d58fe4, 0x3f24a9089131326b),
        (0x3b7a0d70ba412e64, 0xbeff71b80a68e993),
        (0xbb11a7a28f6d7794, 0x3e9b91b885fa211a),
        (0xbb42339bfc23dfbc, 0x3ea32030cab757da),
        (0xbb1cda1488302a7e, 0xbe76157aada72026),
        (0xbadf9a0d5ca2457c, 0x3e31131ffd0ba6ca),
    ],
    [
        (0xbc7ece76656bab74, 0x3fec5be6e950c0b7),
        (0x3c63bb57e740537e, 0x3fd2e8a012e0fa7b),
        (0x3c0575dc0334f2f4, 0x3f83ff0526acf1d1),
        (0x3c044dc560ec8f12, 0xbf74b291f390e4df),
        (0xbba350c48d6165b4, 0x3f224f839f50e0d8),
        (0xbbcf4d7854c8f79d, 0x3f277180d211eb44),
        (0x3ba94de841c700c9, 0xbf03d68928731504),
        (0xbb5b205425b9350c, 0x3ec426773f6ea48b),
        (0xbb1144f74a129450, 0x3e8ffe1e219179b5),
        (0xbabc5212976e4640, 0xbe6a9699317cdb6b),
        (0xbab5cec1a7ad7650, 0x3e25a54cb77230ab),
    ],
    [
        (0x3c7d3f135943435e, 0x3fec5bd2eb61db6c),
        (0xbc61a1b9a1340f02, 0x3fd2e94353bc742e),
        (0x3c19472444a43534, 0x3f83d9826b0583dd),
        (0xbbf12099cc113f3c, 0xbf7460d083cf2916),
        (0x3bb25fb6f0143753, 0x3f15ff639d8c7e95),
        (0x3bcede86c1446be7, 0x3f2b084187ccc491),
        (0x3b9a4dd307e02614, 0xbf08bbc0c1452f04),
        (0xbb3417e35857f4d0, 0x3ed33caa76ba5931),
        (0x3b1f52eb65326bfc, 0xbe7a134a03fb3e51),
        (0x3ad82ac5fbd7ed1c, 0xbe545f84b2d562ea),
        (0xbaa952213eabb426, 0x3e15c65f270ddf3a),
    ],
    [
        (0x3c61314e0f36eae0, 0x3fec5bb0fabf7432),
        (0x3c4a7c9c8f10f7f0, 0x3fd2ea43cf632902),
        (0xbc2bb7ae41d5a847, 0x3f83a2f96236fd49),
        (0xbbe33588677f3160, 0xbf73f2d3185d3b37),
        (0xbb893c2f894e5ec9, 0x3eee57818d9bc48d),
        (0xbbcfddea70d9e657, 0x3f2f2a9378e5af2f),
        (0xbb63ef176f255500, 0xbf0df3787dbe8741),
        (0x3b655f1aa127557e, 0x3edc459e3ece2d4d),
        (0xbb1e1661ae65e8e0, 0xbe9b0fc5cfefa97b),
        (0xbad66f3fc66c8a1e, 0x3e3d44dc6438f8b4),
        (0x3a8d0e6f53fcebaa, 0x3df3e3080e36d5ab),
    ],
    [
        (0xbc83c010ea9374dc, 0x3fec5b7f0b87a9f9),
        (0x3c6a6947b642049a, 0x3fd2eba2164b914b),
        (0x3c2634e3ab1d746a, 0x3f835dd772e0ef48),
        (0x3bf0782b17d77b30, 0xbf737167e3a38e85),
        (0xbbb40bdd48addf07, 0xbf1016d6fb297d24),
        (0x3bcf4fce5e515ae2, 0x3f31adaaa086b765),
        (0xbb8667e90e887a10, 0xbf116e09c64e2aad),
        (0x3b733b8f1b2232c6, 0x3ee2148b515bbd2b),
        (0xbb3bb2c4ed26a2da, 0xbea5da89dcd96f7f),
        (0xbafdf9fe30fc648c, 0x3e5c23c03edd43fc),
        (0x3a68ee4c14603a48, 0xbdfb0412417cab57),
    ],
    [
        (0xbc773b1b718353b8, 0x3fec5b423b9914bf),
        (0xbc7f621dd963a3cd, 0x3fd2ed2f4cdcf43d),
        (0x3c1377fcfefe24aa, 0x3f8314d842c3c294),
        (0x3be8e3cbd7aeb3f0, 0xbf72f22b0bee15ab),
        (0x3bc496dcb0a74226, 0xbf2124f7dd94863f),
        (0xbbc478f070fc4cca, 0x3f3376cd8b422ad4),
        (0x3bb72b86098b27ca, 0xbf13609490beb9b4),
        (0xbb8a94963c37f01f, 0x3ee4fe73c72cd39c),
        (0x3b4eb88aba09a145, 0xbeab93d2727633c8),
        (0x3ada9fc93c355918, 0x3e64bc38f4bdd701),
        (0x3aacb4db95da1717, 0xbe0b7c042bc74acf),
    ],
    [
        (0x3c7468673688468e, 0x3fec5b0e0b4ba59c),
        (0x3c63faba1ee6b95a, 0x3fd2ee6e13906790),
        (0x3c25d66fa927da0f, 0x3f82de1072840d12),
        (0x3c049a24d8185b76, 0xbf7298e1fdd2f328),
        (0xbbcb7522c6abdf2b, 0xbf271d739ebb595c),
        (0x3b781acdc996cf00, 0x3f348f3e4ad28bed),
        (0xbbb072bf3c89d176, 0xbf147e86a40b207b),
        (0xbb7326b6cefec84a, 0x3ee68e6da7092266),
        (0xbb4ab0ed312c8bf6, 0xbeae725d99148642),
        (0x3ae0aa816b363984, 0x3e67dbdaa9091ad7),
        (0xbab2ce220dadff17, 0xbe10cdaf22c2927b),
    ],
    [
        (0x3c59b93c25ba7460, 0x3fec5b0cbe5e774e),
        (0x3c76bace4b68f17f, 0x3fd2ee7808bb5f14),
        (0x3c23621dcf18db27, 0x3f82dc0fb77c520e),
        (0xbc02d3c316b92c3a, 0xbf729538f26e0dcd),
        (0xbbb5af2640454844, 0xbf2761ad24928630),
        (0xbbbf891c477ebd78, 0x3f349c95434125d0),
        (0xbba67df7fbd6d762, 0xbf148cc92ace3e89),
        (0xbb8134dd93b8d72a, 0x3ee6a3128d6f907c),
        (0xbb480c96baa85bb3, 0xbeae99327a49a987),
        (0xbb010257aa03b053, 0x3e6806c7c36a2043),
        (0x3a8d675538737ba0, 0xbe10f818a58178e7),
    ],
    [
        (0x3c4a20c2ffd8c330, 0x3fec5b8650dc1b3c),
        (0x3c62ceb5ea6912b2, 0x3fd2ebf4d4343027),
        (0x3c16415358b3f530, 0x3f833bcb9ed1448b),
        (0xbba8e783f7cfa180, 0xbf731c5b9abc5061),
        (0xbbaae1179ef013fc, 0xbf1f1c82ab22093f),
        (0x3bd7061ebab8bd73, 0x3f335e45d67f5aad),
        (0xbbb3588d8714539f, 0xbf1373beb7a74ded),
        (0x3b7fb635c236f1be, 0x3ee54eaf0a4c3c7d),
        (0x3b4b413e2552f1f8, 0xbeac7bf3734a2753),
        (0x3ad1966368233040, 0x3e6608a4dfca5ed0),
        (0xbaabd52ab1c1dbd7, 0xbe0e8e7eadc45948),
    ],
    [
        (0xbc86c6b99854f4ba, 0x3fec5ce2559d0e27),
        (0xbc4a9e39820df128, 0x3fd2e52f5edc3a75),
        (0x3c27e98d97a9a153, 0x3f842eb29566ca99),
        (0x3c11cc01d593a0ec, 0xbf745f29c9e85745),
        (0x3b89afdb819cd2f2, 0x3ef05af782dbcf48),
        (0x3bd94f533f217e09, 0x3f30bc4a31a29779),
        (0xbbbfbe37dbbc71f8, 0xbf11437d0d41d892),
        (0xbb67d7e84495e1e8, 0x3ee2cfcf4d336454),
        (0x3b3d0270024aa634, 0xbea8bf815c6422e7),
        (0xbb05654d572091fa, 0x3e62b7e50b8b90f7),
        (0xba85f715ca71b7dc, 0xbe094267189abccb),
    ],
    [
        (0xbc8b568ee19f600b, 0x3fec5fa0fcc15e00),
        (0xbc64ae1ca196be12, 0x3fd2d850584e3d92),
        (0x3c0a1c38b8779b7c, 0x3f85e1633267448c),
        (0xbc13b2df368daa76, 0xbf767f05f772e0a9),
        (0xbba0052ee0bdb2ec, 0x3f2df5e6488ca6b4),
        (0xbbc5d74cdcf0270c, 0x3f299bbf35dee9e2),
        (0x3b96ad64b65e89ec, 0xbf0c5fcccc6c2660),
        (0xbb7ddbaa4fd30031, 0x3edf04a61deebc6f),
        (0xbb4641f56fdb0c8d, 0xbea417ec3b158cd4),
        (0x3af812e2551e8ff5, 0x3e5da8ee1deb57d9),
        (0xba9c21a62c8f20b2, 0xbe036932312c05a8),
    ],
    [
        (0xbc47652f2b249250, 0x3fec6448d67cfe05),
        (0x3c5afdb8fb1ae7ac, 0x3fd2c3bb4abd265f),
        (0x3bf6ea0e9295baa8, 0x3f8870b03cea9b85),
        (0x3c16e6edb6eaa9ce, 0xbf7983ef9ac59092),
        (0xbbd53706eee79aa0, 0x3f40d717aff12a16),
        (0x3b976cca73ed1ac4, 0x3f1f5b3b385c1df1),
        (0xbba92870918744ca, 0xbf050c70db59e05d),
        (0xbb68ce6bbed5291e, 0x3ed79ad9cab6b863),
        (0x3b25baf1eee468b0, 0xbe9e56911c6c7a65),
        (0x3acd5d9a83435b80, 0x3e55e780d4a0464c),
        (0x3a8a364d35d45748, 0xbdfbd379eb2ab90c),
    ],
    [
        (0xbc86c14b725ebb7e, 0x3fec6b4995c9de08),
        (0x3c7fb4771aa6f28f, 0x3fd2a6801486dfd3),
        (0xbc1ddfd7f1a153ba, 0x3f8bdf67d031f37d),
        (0xbc1586107ba99f80, 0xbf7d567e256e9203),
        (0xbbd112a73c31475e, 0x3f4c04519837759b),
        (0x3ba970117820cdb0, 0x3f01e26fbfb35d5e),
        (0x3b917088f90c92fd, 0xbefa7c64efae669b),
        (0x3b65bd710079150c, 0x3ed025b4f44232c3),
        (0xbb3f4dc2dd3bca5a, 0xbe94fbfe22e2526d),
        (0xbad2bf7e2a4b5574, 0x3e4de68ff4d747db),
        (0xba66c7d262b0b8a0, 0xbdf284a620b476c7),
    ],
    [
        (0xbc84f871309252ee, 0x3fec74d76f950dde),
        (0x3c73834d4a6e7629, 0x3fd280c9b1a7e591),
        (0x3c3fa12d907a2b1e, 0x3f9007b78ba255a7),
        (0x3c16d44c8e8e4772, 0xbf80dfb353df5a7b),
        (0x3bfb84839bc97e6c, 0x3f541ace9d6f0acb),
        (0xbb9f14a16e84e7e6, 0xbf0c5b9486ce16f6),
        (0xbb624dbbbdce6efc, 0xbee6845e8710cd70),
        (0x3b6b59eb1f7dce35, 0x3ec289bd217664a3),
        (0xbb1a89e7d7c9c484, 0xbe89a757f8976281),
        (0x3acb4ae14dab0160, 0x3e426e9030e70fe7),
        (0x3a66a0ff13406f8c, 0xbde685814eb9c1cd),
    ],
    [
        (0x3c809dc339e7995b, 0x3fec80c5a9555a89),
        (0xbc7ac33f6b3ca912, 0x3fd25430220cdd40),
        (0xbc1d4879d501b850, 0x3f92600eb46b8925),
        (0xbc2356327e3c25bb, 0xbf8336697f13a6f5),
        (0x3bda184d42970a70, 0x3f5a3a7bf90daf85),
        (0xbbcf8a4f720606fa, 0xbf2216381ceaccf0),
        (0xbb5d74978d8f4ff4, 0x3ec3acc294571d2d),
        (0x3b40f758a5d05eff, 0x3eab35536442f032),
        (0xbb1ec9e02f4c63ac, 0xbe78f2289217918e),
        (0xbabce0fe6cf01f98, 0x3e3350c3425bfb87),
        (0xba4f5a4d99818b90, 0xbdd8030b1ab1d204),
    ],
    [
        (0xbc8d02acc1cc01da, 0x3fec8e6875ca6326),
        (0x3c68a17807900ab2, 0x3fd223d750e2a6ce),
        (0x3c3163ca3d33dbaf, 0x3f94c9473e76f76e),
        (0xbc098c145f9a6988, 0xbf857e3609470780),
        (0x3be47f0b24ee33a0, 0x3f5fe44219ffd11d),
        (0xbbc84789e8a20cf6, 0xbf2bbb7875215acb),
        (0x3b826e3c4224937a, 0x3eebbd791e5dd7a0),
        (0xbb3acd5f8da0e7f8, 0xbe93a6327ea04bd4),
        (0xbae90714b4795a94, 0xbe54e507e484f249),
        (0xbab1e85380873c6b, 0x3e1b7573e2bacf04),
        (0xba3301dce6665228, 0xbdc3b8ad84d29515),
    ],
    [
        (0x3c8d598cc241ff55, 0x3fec9c85c70ba99b),
        (0xbc65e89f36890f9c, 0x3fd1f44f0f0625b4),
        (0x3c367cbc3334c914, 0x3f9709a35c721473),
        (0xbc23c533c2439634, 0xbf8783fdd8cab2f6),
        (0x3bff4430c6d372ec, 0x3f6254c211749b8b),
        (0x3bd7b84698e1faad, 0xbf31b9854d15a252),
        (0xbb8cd24e4e9b2656, 0x3ef68a7163ed7349),
        (0x3aee567652b74700, 0xbeb24689d2fed6d7),
        (0xbaaf24ed7d5f8040, 0x3e6096c6454ced2d),
        (0x3a94b5bb048a5dc6, 0xbdf3d8ad529aec47),
        (0x3a352f915f1c25ab, 0xbd91ca14681e58d4),
    ],
    [
        (0xbc74394db20486d4, 0x3feca95a4f0eb301),
        (0x3c4a618c39437380, 0x3fd1cb356c162992),
        (0xbbd69159680e11c0, 0x3f98e3b24dd576a4),
        (0x3bb8f7d83288ce80, 0xbf891917845064d2),
        (0xbbf78d9838298862, 0x3f641b308822fb3e),
        (0xbbc321121160c9d8, 0xbf3474c17c3e0cfb),
        (0x3b9671925655ca8f, 0x3efc6107868e72b2),
        (0x3b46dc53b07e8e38, 0xbebad58367e4fcc3),
        (0x3b0b188021c3c3b6, 0x3e7087856ee75ad1),
        (0xbaad266b1a1b870e, 0xbe17bf1e1306c8f8),
        (0x3a4abb0faac45373, 0x3dadad8d29b6235a),
    ],
    [
        (0xbc7b6735f38dcae0, 0x3fecb2b42a201841),
        (0xbc71582a96911b64, 0x3fd1aea941ad3474),
        (0xbc1a5e42a8fa5814, 0x3f9a1d7ee70c5812),
        (0xbc2046c34fb353f0, 0xbf8a18a3b401e573),
        (0x3bf7ffd5734be186, 0x3f652c60953fad12),
        (0x3bdd67e65789eb7f, 0xbf360556f51f1a8d),
        (0x3b9c078fde66a698, 0x3eff90fa5f587ec6),
        (0xbb3b345af7af1394, 0xbebf495ae99135f7),
        (0x3b1ef4298de4a753, 0x3e749ca3314eb91b),
        (0x3ac0bc479cb04d48, 0xbe204f74fb426011),
        (0x3a540203e5d5fe1e, 0x3db78557e884da1f),
    ],
    [
        (0x3c7b9948887e3e30, 0x3fecb620c520b78a),
        (0xbc5cab423bfd4cb4, 0x3fd1a4a30f1a92da),
        (0x3c2937d3e12e5ef0, 0x3f9a8725b90119cc),
        (0x3c2a939091181278, 0xbf8a6b215fafec97),
        (0x3b842353662cd800, 0x3f6580eb53280d97),
        (0x3bd5dbe311f5e11e, 0xbf367c2d0446d766),
        (0x3ba105d1260b0e81, 0x3f003c7ffe8bc37c),
        (0xbb5bdc4485e10110, 0xbec04002440fd45b),
        (0xbaf45c45a6300d6c, 0x3e75ada1d2518cd8),
        (0x3a9e8e805aba9430, 0xbe216bcc91193d8a),
        (0xba49ad660ab34b8e, 0x3db99a7a2668e27b),
    ],
    [
        (0xbc2947bf41bc9e00, 0x3fecb126f017035d),
        (0xbc7899059f5b8bb1, 0x3fd1b25105f6bdf3),
        (0xbc0895d0113bfb18, 0x3f99ffbf6823d4f5),
        (0xbc0f10a553f5d368, 0xbf8a07d8fb6fb3de),
        (0xbc0c7ec3a21f454e, 0x3f65215c13d9b6ff),
        (0x3bd1b601cf9453e4, 0xbf35fe063a62e384),
        (0x3b8827981ea2380a, 0x3eff91aca599febb),
        (0xbb2fc16dac065cc8, 0xbebf5d1e288c9e5c),
        (0xbaeef186161095a0, 0x3e74bd8a1c9555bc),
        (0xbacc403521f2eaf1, 0xbe2080eb36ed965e),
        (0xba3f86e752c89df8, 0x3db7fcd3a5bdb4d8),
    ],
    [
        (0x3c8bcee7c8181d39, 0x3feca18848848e82),
        (0x3c69fc813308a73c, 0x3fd1db84d997da00),
        (0x3c3c53850ba9a712, 0x3f98786cc1d7bdc5),
        (0xbc2ca52fc8e5b866, 0xbf88f4811c08cd00),
        (0x3bff40da3a5c6bdc, 0x3f64230b2277791f),
        (0xbbca96457825fbbc, 0xbf34bbd65de2655f),
        (0xbb8f50c40c736b46, 0x3efd5ab0bde82aa8),
        (0xbb50eafc87b58e98, 0xbebcb0d4a3c5aff1),
        (0x3b089e7298344bb0, 0x3e729f7e0e19e149),
        (0xba7bdb04058a0820, 0xbe1d07eae288fa78),
        (0xba4b0253c12941ea, 0x3db4a07f49c5130b),
    ],
    [
        (0xbc89edfc54aa2483, 0x3fec857c1cd41af6),
        (0xbc5a659387945ca0, 0x3fd2225424e8bcf6),
        (0x3c377fc2e3bc7889, 0x3f95f4c4f8ed59c3),
        (0x3c2c4286b497cf7c, 0xbf87430db00b9afa),
        (0x3c073f64e00247cb, 0x3f62a3e0f44a96a2),
        (0xbbbd945716fa0818, 0xbf32eb40cc8f3c79),
        (0xbb89740359a8ca0e, 0x3efa4c36e442171d),
        (0xbb15318efd8f9b50, 0xbeb9290343025508),
        (0x3b0452efb2ecf7c8, 0x3e6fe4933deba02f),
        (0x3abe6d64af899514, 0xbe183869735ef3a0),
        (0x3a34e4c2dbab070c, 0x3db0bc589c565cf5),
    ],
    [
        (0xbc79fbf2f033ddfa, 0x3fec5be1ae114ebf),
        (0x3c62fd50833dbe24, 0x3fd286e5752eafab),
        (0xbbd5a1098dc5b600, 0x3f92897c1dc47bc3),
        (0x3c1904c95a070666, 0xbf850eaed8497ba0),
        (0xbbd04ac48084a568, 0x3f60c6331075f2b6),
        (0x3bbf3f5b46bed4bc, 0xbf30c0b464b7bc75),
        (0xbb98f7dad74f10c4, 0x3ef6cdf21e81cb9a),
        (0x3b44e287afdd458a, 0xbeb54c027ef829be),
        (0xbb0e9493b04030bd, 0x3e6a48ce7c9a8f3a),
        (0x3ab2e43f966ce1b5, 0xbe136513318f7913),
        (0x3a1693d5d1266bc0, 0x3da9ff3e55e5505b),
    ],
    [
        (0x3c194781c55e3f00, 0x3fec24612d8075f9),
        (0x3c42c7b224a571e8, 0x3fd3077421970e7e),
        (0x3c2f8a4e5c0c1a72, 0x3f8cb2bb0e6bd65c),
        (0x3c26ce9b18985937, 0xbf82784bfab50a33),
        (0xbbf575cf19a4e653, 0x3f5d5a00e338fbc3),
        (0x3bb58b5f972663f2, 0xbf2cd6470bd0df26),
        (0xbb9d14973ed1a406, 0x3ef3329bb4ddacb9),
        (0xbb594a948357e8a2, 0xbeb17992005b48da),
        (0xbae1a67f3edd9b50, 0x3e64f7cb2aa0a2a1),
        (0x3aa41767e302bcd7, 0xbe0e0619d8c4b803),
        (0x3a42aa74db3d3d98, 0x3da37e072fc79210),
    ],
    [
        (0x3c8d85ecbc120409, 0x3febdf79b3f36264),
        (0x3c4ae0e5eb5f4e28, 0x3fd3a081ec9e8dc3),
        (0x3c263a71c416c207, 0x3f8322a212289954),
        (0x3be52b87741ca630, 0xbf7f4624e1cf93c2),
        (0x3beb1990f8049eec, 0x3f58f1f394dd9af0),
        (0xbbc35bb151b25d75, 0xbf2822f4710adeee),
        (0xbb887c15268e3c40, 0x3eef6e32a041feb1),
        (0xbb4c7bc7c59ec68c, 0xbeabdf462f9e52f8),
        (0x3b054e47e872ed22, 0x3e603f5ed0b63b43),
        (0xba8c028decc6d7ec, 0xbe068f73246295da),
        (0xba3dbbf54cb0eec2, 0x3d9c5cdde2869e86),
    ],
    [
        (0xbc5b64600e93c3c0, 0x3feb8e7bcdfa2551),
        (0xbc5edb222388a5a4, 0x3fd44d2c26cbf7ab),
        (0x3c150066d9ee763d, 0x3f718ffba24f3952),
        (0x3c09a588d15d0ddc, 0xbf7962e4ef5c450f),
        (0xbbfea7fbc24ad3bd, 0x3f548ce8089a5348),
        (0xbbbb19fd9ed05e78, 0xbf23a326550eca65),
        (0x3b4883cab8f6a4d0, 0x3ee908398ae19492),
        (0xbb3dae34b83d0a7e, 0xbea5a1d18b74c1ad),
        (0x3af6481f3bef8e86, 0x3e5881b400db6b43),
        (0x3a9febede716e6a0, 0xbe007fd85744e496),
        (0xba3e753baebb1cb9, 0x3d94159b20d20045),
    ],
    [
        (0xbc8e0384101b69ae, 0x3feb3372978b846c),
        (0x3c7b389bd1e1869a, 0x3fd507973f33deca),
        (0x3be2e93210bce21a, 0xbf4f4d350dde3443),
        (0x3c1dbbd2ec26225d, 0xbf738585a37ac336),
        (0x3be34b6c09c314de, 0x3f50587dfefd189d),
        (0x3bacacf0dbcad6b4, 0xbf1f014a3f2c06fd),
        (0xbb8fcbc2dcbf78a5, 0x3ee362604eb5e17c),
        (0xbb454b555003d9a0, 0xbea0576c9981626c),
        (0xbaf474992319e3e5, 0x3e5200504cc51756),
        (0xba9a6909449d2d57, 0xbdf7846656305e2c),
        (0xba2cc3f7de9c46f8, 0x3d8bbadfc202f815),
    ],
    [
        (0xbc8a3a50aa1d0747, 0x3fead0ff0244e221),
        (0xbc7a4fcbad89546e, 0x3fd5c9637406d596),
        (0x3c19bbcf5493a8bd, 0xbf795f996b9bda39),
        (0x3c0b49da59645f55, 0xbf6bc68547b5094f),
        (0xbbdb42f1472d8fc6, 0x3f48ed03525fcc78),
        (0x3b773bee95e6a5c0, 0xbf17aa1e224a084b),
        (0xbb7dce71fb3e3715, 0x3edd215cc70f90bc),
        (0xbb2a0ef6b971411c, 0xbe980113baf025cd),
        (0x3aee70cf25ebaad4, 0x3e49be8d01e22c7d),
        (0xba94bf3997882434, 0xbdf054d1d63dc91a),
        (0x3a20f0241013c27d, 0x3d82ab14512ab887),
    ],
    [
        (0xbc8f9b01fd279096, 0x3fea6a29d58c33b7),
        (0xbc674dce8d0d0f3c, 0x3fd68c1eb8e2979d),
        (0x3c1bfcc8cbb07d48, 0xbf870f223a0c0167),
        (0xbbfb9ab59aae5a80, 0xbf614c2e57681df0),
        (0xbbd2b24814ac2946, 0x3f41faa38f77e2dd),
        (0xbbb53e8ed6013a54, 0xbf1158f6fd950634),
        (0x3b682bf413594436, 0x3ed526b8cc5a388b),
        (0xbb2f4bc0688a4900, 0xbe9117b230bc51cb),
        (0xbae98263a8ee88cd, 0x3e41e2b3a3f437f8),
        (0x3a78e8eb32b2b25c, 0xbde61231934d9184),
        (0xba1a8267a0ec97a6, 0x3d787cedf94e959b),
    ],
    [
        (0x3c77d79c50a3711c, 0x3fea0231475ff3ae),
        (0xbc76363fa4e751ce, 0x3fd749aa5223f7e6),
        (0xbc3ba545d09d93bf, 0xbf9063ae7ef70c82),
        (0x3bd3d8a5dcae02b8, 0xbf4f618f89fa450f),
        (0xbbd20ab97faf56c8, 0x3f37e458b1e356d2),
        (0xbb86ee12886504d4, 0xbf0821cfdc163182),
        (0x3b2399e77fb2aac0, 0x3ecd75466a96fffa),
        (0xbb2ba6075e89c324, 0xbe87796133348897),
        (0x3ade02e57201493d, 0x3e380bfa3749564d),
        (0xba46d184faf9c670, 0xbddcee3600927b2c),
        (0x39f3dd4c231ece36, 0x3d6f362ec2a3967b),
    ],
    [
        (0x3c735b83158e076c, 0x3fe99c56d0c67edb),
        (0xbc7a0b939d383a3d, 0x3fd7fc8d884ba6f2),
        (0xbc258d70b80083a0, 0xbf94cedb0ec61a6e),
        (0x3ba17e34a4e241e3, 0x3f0bcb4f74b08e2f),
        (0xbbbd6ec88c065d10, 0x3f2b6b788359e8dd),
        (0xbb940711b6ddbb99, 0xbeff16fca1811824),
        (0x3b664cd0d6355e5b, 0x3ec3660dc6b130e1),
        (0xbb1e6e3b0d706c32, 0xbe7ec91c367ea244),
        (0x3ace61b5d0d8a422, 0x3e2f0cc3ffc61fb0),
        (0xba4afae6d7bdc6e0, 0xbdd2476a6857058d),
        (0x3a00d53a0573b0fc, 0x3d633a7716320ae7),
    ],
    [
        (0xbc79381c4b156290, 0x3fe93bb13b9992ac),
        (0x3c7970515413bd0e, 0x3fd8a031c4b5878f),
        (0x3c2031b5b4ec6b42, 0xbf98b46c9b7757e1),
        (0xbbc736951053a998, 0x3f4de4c5bf840851),
        (0x3ba8c149b58a4e02, 0x3f15754d3047c4dd),
        (0xbb949f7b0a34b5b6, 0xbef18508262de66c),
        (0xbb45552c936dac08, 0x3eb778e548c6b669),
        (0xbb1a6048f183d296, 0xbe72eab94b8e28a2),
        (0x3ac7391c2bf764c2, 0x3e22fc01dac54242),
        (0xba57caf213001686, 0xbdc6050b8d7ebfb9),
        (0x39ec1d99f5c2d0ac, 0x3d56b075f6914b50),
    ],
    [
        (0xbc6bef6c010a9dc8, 0x3fe8e305fd2cb54e),
        (0x3c57932d301d71e4, 0x3fd9310711c87531),
        (0x3c386a44ecd2809e, 0xbf9c0829c8db1297),
        (0x3befcbf5dbe22972, 0x3f5a8ae87061dead),
        (0xbb7c9eb3c41756f8, 0xbef44394ab78a55e),
        (0xbb7a0c67c82446cc, 0xbedc78b9f90cda78),
        (0xbb420fd732d8f516, 0x3ea847cae47a2a7b),
        (0x3afb56e020c7a39e, 0xbe64e6bb322f4510),
        (0xbab3903c2be6b225, 0x3e155d1a9adaec94),
        (0x3a44a03f19abf2cc, 0xbdb8bcefe707e8fc),
        (0xb9d2417a35fd5cf8, 0x3d492f55542093f8),
    ],
    [
        (0xbc862c4896b0b83d, 0x3fe894abe4a5b9dc),
        (0x3c7fe5c1c461460b, 0x3fd9ac922ad51dca),
        (0xbc33c291e0f24f05, 0xbf9ec58118c16c40),
        (0x3c0cf0b67c87e94e, 0x3f61e13d56b8940f),
        (0x3b6a790492e66540, 0xbf196af8349e4224),
        (0x3b31fa44d2bbd27e, 0x3ea2c42b70c9face),
        (0x3b2da20edbf59d2a, 0x3e9026f15ff2ee68),
        (0x3ae76f3d337ed97c, 0xbe526e097fd57d38),
        (0x3a9b983a79d51a18, 0x3e049a10a6c5b670),
        (0x3a3dc119a1c2f37a, 0xbda8a67c2aff9c17),
        (0xb9b2a4fe2b205130, 0x3d394c38265362bb),
    ],
    [
        (0x3c77751441c8d3b4, 0x3fe8527813695aa2),
        (0x3c684eaa21e959ac, 0x3fda1166ea70106b),
        (0xbbdf4a6612c53b00, 0xbfa07734e6653b74),
        (0x3c0c7623498c8faa, 0x3f6563a6d917beff),
        (0xbbbd20a58a820126, 0xbf2431a6af0bf8de),
        (0x3b7d336f20d13d06, 0x3ed83dd6dda34654),
        (0xbb0b79b53e2c9b8a, 0xbe785be48d0ea29c),
        (0xbabeae4dddf12aee, 0xbe277cc09aefafd0),
        (0x3a59b67c103ee0d0, 0x3de9bcf4059586a2),
        (0x3a36708298b1f001, 0xbd92977be7d90308),
        (0xb9995f674b559478, 0x3d24a39363573224),
    ],
    [
        (0x3c88059266015c63, 0x3fe81db53af85c81),
        (0x3c789ce0c91db2ea, 0x3fda5f12f3ca50da),
        (0x3c4fff4eb90f91b4, 0xbfa1450b1759f5fd),
        (0xbc0a5bae5f820112, 0x3f67ea33ae8225ad),
        (0x3bab3e1e966adef4, 0xbf296683eed1efcc),
        (0x3b558fbcb75a4300, 0x3ee37b35afee8bcf),
        (0x3b378b11a48054f7, 0xbe948b0f763cdd6e),
        (0xbadc68d151c5bcb6, 0x3e3b2ec7f8804690),
        (0x3a7a42b7c2cfda06, 0xbdd15431166629c5),
        (0x39c2cae40190fb38, 0xbd4254e40504074e),
        (0xb99f9b3ffd3df550, 0x3cfd32cfd9ee6824),
    ],
    [
        (0x3c87852e7149316e, 0x3fe7f7244909eafb),
        (0x3c7d8b1870b59b84, 0x3fda95fcf538479f),
        (0xbc2dd434dbc26fe4, 0xbfa1d1cca085a602),
        (0x3c0f3d9182229bc7, 0x3f6995d566fe00f2),
        (0xbbce4c25eba9cee0, 0xbf2cbb2cd72dbf60),
        (0xbb6230a87de521a4, 0x3ee8091a0ed3ca17),
        (0xbb335f025a60c368, 0xbe9d316349e5762a),
        (0x3aed896b5a4d66cf, 0x3e48db6f436655ec),
        (0xba8d11019695e34c, 0xbdebeca2e7bfe62e),
        (0x3a13d9003f78f398, 0x3d825e2abee6700c),
        (0xb990404712f30786, 0xbd04fd8e7f84648d),
    ],
    [
        (0xbc7d8fda24c8dc12, 0x3fe7df050ce33e3b),
        (0x3c74e2e804ecc588, 0x3fdab73cea883ea5),
        (0xbc2f5e041ad627c8, 0xbfa2244d670961da),
        (0x3c084c14e3d4348d, 0x3f6a887a1549f65c),
        (0xbbad4fb99d51b250, 0xbf2e8f85a842c421),
        (0xbb6484129b1a6f58, 0x3eea7507df06e1f0),
        (0xbb28afff859217ec, 0xbea0d29386ae890a),
        (0xbad0e96cc5515e0e, 0x3e4e7874a63969fb),
        (0xba9457f9482630cf, 0xbdf29b66626d984b),
        (0x3a061faa1b0f8ae4, 0x3d8b7a97aa5e6073),
        (0x39b8132f149882ca, 0xbd1289bc81c39d03),
    ],
    [
        (0x3c7858d5859b0790, 0x3fe7d524fa022593),
        (0x3c7ab8681f9b2dda, 0x3fdac471728a6e5c),
        (0xbc392a31bd2c45e0, 0xbfa24416aa73c1ed),
        (0x3c0d03e98625a176, 0x3f6ae329e0be0f25),
        (0x3bb3ba40a20c6278, 0xbf2f39530a88b387),
        (0x3b683affc9a4f36c, 0x3eeb4f0eff41c408),
        (0x3b4b93014e8d4280, 0xbea194ff496f4fa6),
        (0x3affa9cc8e999f15, 0x3e502a0196d40303),
        (0x3a87d9e18ef0015c, 0xbdf4191a6c0fa6f9),
        (0x3a016447bf89fbf8, 0x3d8e50d97a2071b0),
        (0x39a41134a604833c, 0xbd14f7987074c37a),
    ],
    [
        (0xbc8849b77320b1d6, 0x3fe7d8f21fcc2d5c),
        (0x3c6e500d1903dbf0, 0x3fdabf9588f99816),
        (0xbc41e8febc95a3f6, 0xbfa238e8af85956a),
        (0x3bf7cb20d4422e6c, 0x3f6ac4adc7f7de78),
        (0x3bcc4e80d908858a, 0xbf2f02c60cfb5d78),
        (0x3b8e622bcfcd200d, 0x3eeb0c1f999348b0),
        (0x3b38a070b3ab8ed8, 0xbea15bf677ada740),
        (0x3abb3aa525a7aa40, 0x3e4fceb78e014b78),
        (0xba88b19b0e21f96c, 0xbdf3b2e2d550cf5f),
        (0xb9c60dd540ad3700, 0x3d8d970d5bc2a4c6),
        (0xb9be83c8c31b4a6b, 0xbd145fa013479421),
    ],
    [
        (0x3c79295ebf3ef4c4, 0x3fe7e9900e8c4c05),
        (0x3c717516935a5da6, 0x3fdaaad9baaf12a4),
        (0x3c4c9b35ae24337b, 0xbfa20a56ed057c52),
        (0x3c044bdda20e1933, 0x3f6a48b3b812e527),
        (0x3ba9b9db34d0c628, 0xbf2e2a29e903ce84),
        (0xbb8eca303b9b0d7d, 0x3eea0897d78deb13),
        (0x3b2024794b273684, 0xbea08401e50fb51f),
        (0xbae524c48f70dcb6, 0x3e4de1cd5f227b76),
        (0x3a93df2981146671, 0xbdf241b2a7dd10b3),
        (0x3a20275bd58bf3a8, 0x3d8b078eda0da34e),
        (0xb975173cc6f8cdc0, 0xbd1253ddd72c126b),
    ],
    [
        (0x3c62ceb50bd97224, 0x3fe805ed671a8ed0),
        (0x3c7b6351621a7e0a, 0x3fda888206fd30ef),
        (0xbc4584aecef194b1, 0xbfa1bf7d67de3096),
        (0xbc08df5dab1e3e31, 0x3f69875818cc1132),
        (0xbb95e8f170b42d00, 0xbf2ce258acfa7ad8),
        (0xbb7ce9c19cd3375a, 0x3ee88b766706b93c),
        (0x3b3b55602543baa8, 0xbe9ea08995007a03),
        (0xbad3cfda551ad0a4, 0x3e4b3836accb970b),
        (0x3a7ce45c5bf4a770, 0xbdf052539f32ed36),
        (0x3a0d7e61158a35fc, 0x3d87b2188a7de05d),
        (0x39aab32ffc3fe31c, 0xbd0f7c473b9d736f),
    ],
    [
        (0xbc76c7483e675afc, 0x3fe82cd81ce66983),
        (0xbc5ef5d3caaba448, 0x3fda5aca2a9e1224),
        (0xbc4a4d027a0a8332, 0xbfa15ecf0dfd892e),
        (0x3be2c1d3462002d8, 0x3f689503837e3442),
        (0xbbc509f8a68e8ca2, 0xbf2b53b6f662cf45),
        (0xbb60f335fd78f46c, 0x3ee6c9c7668886b1),
        (0xbb3a5a0cabb87303, 0xbe9bdff1f2d05298),
        (0xbae3d6fb4768ef6f, 0x3e484322f27254ec),
        (0xba5cfbb17d2ed970, 0xbdec78e7274dd815),
        (0x3a0fae6fdd22043c, 0x3d8435a56ec10a68),
        (0x398a0afc8fdd84cc, 0xbd0a3d84b2a469ec),
    ],
    [
        (0x3c85275019a63bb1, 0x3fe85d0f9ead23a9),
        (0xbc7974d5f2d0ab34, 0x3fda23d053d2b1f9),
        (0x3c25be352012ca48, 0xbfa0edf91eeb8a5a),
        (0xbbfa726a80174ca0, 0x3f678284e4bab95d),
        (0xbbcceccff8d62cba, 0xbf299d7803f58699),
        (0x3b20eb35873a9940, 0x3ee4e9f7283f6640),
        (0x3b3641fc5b936877, 0xbe9906486da98e29),
        (0x3aea438a4fcdd9f2, 0x3e454a362a3889a6),
        (0xba82ae66c2606eaf, 0xbde867553e123f52),
        (0xba231385b8b89c0f, 0x3d80e8b863b8cec3),
        (0x399dbb221e9dfdb4, 0xbd056bb50a6179c5),
    ],
    [
        (0xbc8345a68bce03f8, 0x3fe895541a035cf4),
        (0x3c6a9a13b818bbe8, 0x3fd9e58630317028),
        (0x3c3e5e56ece03e20, 0xbfa071d825df20c5),
        (0xbc043060f7b87f82, 0x3f665d556fbb2b9e),
        (0x3bbb55c0244c2894, 0xbf27d6fef71eedec),
        (0x3b806a3db3cffa6e, 0x3ee306dbc230ea08),
        (0xbb2fcb3bd608fa04, 0xbe963cfb5eb7dc39),
        (0x3ad8bdca1f8849c6, 0x3e4277fcbf00c0f2),
        (0x3a79b5a7f6701dda, 0xbde4a77f1e97bc2a),
        (0x39ee8bc647b19098, 0x3d7be97fa139ec70),
        (0x39a742e93993d7e6, 0xbd013be949b0c1df),
    ],
    [
        (0x3c85a304157923b2, 0x3fe8d4728500ffee),
        (0xbc71876145eae8b8, 0x3fd9a1a7b920519b),
        (0xbc3d2ec62d32922e, 0xbf9fdcf4fe2e6866),
        (0xbbcb05a4e91bc710, 0x3f652ff5c4a490a2),
        (0xbbc9fb86475d7c78, 0xbf26113d24d89dd2),
        (0x3b6e06275e8ce9b4, 0x3ee1325b7e36d29e),
        (0x3b2e12813f06a494, 0xbe939d1a60ad6f51),
        (0xbad3005982fa855a, 0x3e3fc676f4a347ee),
        (0xba85afc3d21b71be, 0xbde152903c9bc0b8),
        (0xba1be795cc3bb4cd, 0x3d76d08684fc4f40),
        (0xb99979de162142b7, 0xbcfb72c9bdfebf2e),
    ],
    [
        (0xbc87e105ec9ca5f4, 0x3fe9194d6629e509),
        (0xbc79c00221836f35, 0x3fd959b6e47cc1cb),
        (0xbc26c9c009d62078, 0xbf9ece59214cf137),
        (0xbbfe20f5fddc5310, 0x3f64025702ca8fc4),
        (0xbba84afb784aa07c, 0xbf2457f85b9b3831),
        (0x3b54ea926ad5167c, 0x3edeef4e272f250a),
        (0xbb023defeec5e0a0, 0xbe913432dc663e67),
        (0x3aae60197d5217c8, 0x3e3b2b72ce97aa39),
        (0x3a63141e2e6f5022, 0xbddcde4ddf08d4ea),
        (0x39eca6549fac9060, 0x3d72854850b02948),
        (0xb939a6cb39aa2600, 0xbcf5b3efba807911),
    ],
    [
        (0xbc24d27ad1e68c80, 0x3fe962e2905556ed),
        (0x3c69998b03a75cee, 0x3fd90efb3eca9aba),
        (0x3c3c5ac4bdd68696, 0xbf9dbd168f65fb7e),
        (0x3be519a7a0660ba4, 0x3f62da45c6e72103),
        (0xbbc8b81ea1bc7080, 0xbf22b2ecd5924135),
        (0x3b5e56067f09a9d4, 0x3edbba1394728855),
        (0x3b28207c17005b80, 0xbe8e0ffed775f6e9),
        (0xbadbacdffd118992, 0x3e372225c30c46fa),
        (0x3a68218e8f652ab4, 0xbdd7f276a6d4d262),
        (0x3a0144bf6c21cae7, 0x3d6dedf685adbda0),
        (0xb99078cdaa8ca380, 0xbcf113f00b9fe725),
    ],
    [
        (0xbc712c24f9d2f218, 0x3fe9b04e3301ca38),
        (0x3c7193d913e4e618, 0x3fd8c28470534676),
        (0xbc3677a730753df1, 0xbf9cad33f35e2755),
        (0x3bc11212e8675ef0, 0x3f61bbd0172a316b),
        (0xbb93d13eee592c20, 0xbf2126c548b5619a),
        (0xbb7f0f63eeeee01d, 0x3ed8cab1036d4dec),
        (0xbb289ac10a4baa55, 0xbe8a32410f19bdd5),
        (0x3ac451ab8a7a47d0, 0x3e33a420595d0d3a),
        (0xba603784d0bf66a6, 0xbdd3ce7c43e80e82),
        (0x39fe2bb244cfded2, 0x3d681c69081d1b37),
        (0x395917e555865c68, 0xbceacbdfedaea1f7),
    ],
    [
        (0x3c8f0fa86a56e6ba, 0x3fea00cbb7e2c1e2),
        (0xbc63acefc8cc1c66, 0x3fd8752ebfc07ba7),
        (0x3c3e999a1b70ea47, 0xbf9ba1b2cc9437f4),
        (0x3be3a460fc6ec980, 0x3f60a9a1d27c214e),
        (0x3bb37b03b766db48, 0xbf1f6bd0acca9dd1),
        (0xbb713d37e0e4001a, 0x3ed6221851224bca),
        (0xbb207e1b7175b01f, 0xbe86ca231706849e),
        (0x3ad2bf8297bed558, 0x3e30a5c736124de1),
        (0xba727489396341d5, 0xbdd05a979295fac9),
        (0x39f1756e19c37c9a, 0x3d6364167eb132f4),
        (0x3983bb2d132598e9, 0xbce4fd25b8623a10),
    ],
    [
        (0x3c84f280c7337943, 0x3fea53b4eef9f5a5),
        (0xbc69118e2061c5da, 0x3fd827a8c3a5cc4b),
        (0x3c3ed707936633ac, 0xbf9a9cbc621418be),
        (0x3bbc9603743be350, 0x3f5f4aaa94ee28c7),
        (0xbbb7a8e3165c93dc, 0xbf1cc23b919438f8),
        (0xbb7920595035541d, 0x3ed3be2ada53954c),
        (0x3b24880c577104dd, 0xbe83cf0de829e720),
        (0xbac9bba9b94d4f97, 0x3e2c32789bf32b44),
        (0x3a6a7d6fb4480815, 0xbdcafc517db4919d),
        (0x39ff848c09f51077, 0x3d5f2b62427707c6),
        (0x398e7d47b82a2483, 0xbce06e6c75ffb9d2),
    ],
    [
        (0x3c874be4e30f55fd, 0x3feaa8800692a548),
        (0xbc7983ddaa23edda, 0x3fd7da799a85a3a1),
        (0x3c29fd6ca97884f0, 0xbf999fcb692e46c2),
        (0x3bf0a8fd72f30686, 0x3f5d5f6e7ebe838d),
        (0xbbb41d28e076799c, 0xbf1a501fd07cd87f),
        (0x3b5a4d8bed2ad3cc, 0x3ed19aee4bf149cb),
        (0x3b286b20ed1ac9b8, 0xbe8136b705548435),
        (0xbaa2b95c9c1a2fd4, 0x3e27e05b60054049),
        (0xba45b18e400c714c, 0xbdc643aab819d20d),
        (0xb9f127bc1b8ba61b, 0x3d590e09ca6a23af),
        (0xb97b1e2097b4cdce, 0xbcd9bc2e12b23103),
    ],
    [
        (0x3c7f2f0799382490, 0x3feafebcbfb3a5a6),
        (0x3c727a6f0626ebe1, 0x3fd78e0728cbc72f),
        (0xbc0989b2c393e360, 0xbf98abd10da484bf),
        (0xbbf1c8cbe9077ebf, 0x3f5b91fd1b5e71f1),
        (0x3bb2dddefa74558b, 0xbf18135c2255aff9),
        (0x3b69dc72be6abee5, 0x3ecf66cede9d9f9f),
        (0x3afb52ef032713c0, 0xbe7decaae15f192a),
        (0xba9db8b3a1526ca8, 0x3e2439c768f9f33b),
        (0xba6bcb4e3ca70c74, 0xbdc261268dbd2e9a),
        (0x39f22f54fe950e34, 0x3d5427b26d8593fa),
        (0xb96523c3104ba290, 0xbcd42c447ec0cc74),
    ],
    [
        (0x3c80f855a5653f06, 0x3feb56113d9e9fc0),
        (0x3c7901a7f01610ff, 0x3fd7429c0204c3ba),
        (0xbc2879c1b3ea956c, 0xbf97c154c2349766),
        (0xbbd2c40ca2762fb4, 0x3f59e1f11efd1eec),
        (0xbbaad9436855a79e, 0xbf1608ebbb454bde),
        (0x3b5d9d26778908c0, 0x3ecc04604ee7154d),
        (0x3b1604c163265ec0, 0xbe7a06c1e1593471),
        (0x3ac14ff60c7c6164, 0x3e21259f614c0715),
        (0xba22d4163461b648, 0xbdbe602ef33d6637),
        (0x39fbfef523aa8104, 0x3d503bc5a16de542),
        (0xb96ef0efa7439614, 0xbccfac1400ac6db2),
    ],
    [
        (0x3c817e5fae67811b, 0x3febae36bac7427c),
        (0x3c416ec3c6a31ff8, 0x3fd6f86cc3b7fc0a),
        (0x3be68b8723641480, 0xbf96e08ec82e7973),
        (0x3bdb9567557c5bac, 0x3f584e572bac1437),
        (0x3bbf4c36068c245d, 0xbf142d4fd9685b5f),
        (0x3b6fd00e8a412202, 0x3ec903b46ab16552),
        (0x3b1a26353b11a93a, 0xbe76a7ffb613d977),
        (0x3a83fcc3e211ffd0, 0x3e1d1b24e667426f),
        (0xba431eb4941eb958, 0xbdb9227627e5f349),
        (0xb9e5b1fb0b09d692, 0x3d4a30f8c120e1fc),
        (0x396256e383967df9, 0xbcc8e8aa37bc61f0),
    ],
    [
        (0xbc6af2a3b8a6417c, 0x3fec06f659b4d0a2),
        (0x3c72c912d943a127, 0x3fd6af9cc36509a8),
        (0x3c346b1c71fd9485, 0xbf96097db8eb9798),
        (0xbbd6098a353eaa68, 0x3f56d5e207087908),
        (0x3ba7ef357dae1da2, 0xbf127cd98a6a5063),
        (0x3b59d23dfa50e50a, 0x3ec65a59b3e87f89),
        (0xbb1b2a7ac925c26a, 0xbe73be7c669b60c4),
        (0x3abf7a6f9aa49d38, 0x3e18bc66c4d33d25),
        (0x3a598bd8cb8e83be, 0xbdb4d4aee38b7aa0),
        (0x39e8c05a738afb6a, 0x3d452ae72a594d04),
        (0xb9581feb7fc372c8, 0xbcc3a189a1f1d088),
    ],
    [
        (0xbc8b94a3f11b0b1b, 0x3fec6026362273c0),
        (0x3c7a9433928985a8, 0x3fd6684205e2cfa8),
        (0xbc316c22e2ee8975, 0xbf953bf793a414a0),
        (0x3b8eaa45bca8e100, 0x3f5577111d8e7869),
        (0x3bb37d8f271623f3, 0xbf10f3db4ed954fd),
        (0xbb5cffa19b715950, 0x3ec3fe9093dddaa2),
        (0x3b1fcf0f684df6f8, 0xbe713a42e1480d90),
        (0x3abfa83b47f916ac, 0x3e150dad8bd02d20),
        (0x3a59abbe7813943f, 0xbdb14b5382d39865),
        (0xb9efe1edf8eeca76, 0x3d41245f6e4996be),
        (0x3949af3eecb215a2, 0xbcbf03908246b7c6),
    ],
    [
        (0xbc80c31a8863f9d6, 0x3fecb9a6cb682a24),
        (0x3c7fed51d74bff86, 0x3fd622688518051f),
        (0xbc1591ef749caee4, 0xbf9477b6ed4c398b),
        (0xbbce137d55208958, 0x3f54304c2141eeee),
        (0xbbab7a179e1ae7dd, 0xbf0f1d91c60481ce),
        (0x3b55449a00736a6e, 0x3ec1e76e7622605d),
        (0xbaccb03dd24f7810, 0xbe6e1a99fac954a8),
        (0xbab80ff44fecc168, 0x3e11f2a815bce70a),
        (0xba3ce823a0233bd6, 0xbdacc51da262d834),
        (0x397750c051a75c00, 0x3d3bd2e2e3a657bb),
        (0xb95134cc93e44584, 0xbcb88ed08e872b27),
    ],
    [
        (0x3c78ddf4513624a6, 0x3fed1360b92664d6),
        (0xbc6c375ce17d0080, 0x3fd5de14d2825f87),
        (0x3c2f9ef6b2759e44, 0xbf93bc64e699f695),
        (0xbbf5442d5bca96e1, 0x3f52fff6380176c4),
        (0xbb949c6dfb89070a, 0xbf0c9494574d2471),
        (0xbb65ac54bdb2df7f, 0x3ec00ce94926b534),
        (0x3b07c40ed8f854a0, 0xbe6a56ccff5f9038),
        (0xbaa6ab98e2498c16, 0x3e0ea6ea534c6311),
        (0xba4cece43020bd1a, 0xbda7fa106c3a3ead),
        (0xb9c623e1759261aa, 0x3d36a181cda3fbde),
        (0xb957aa56acc34690, 0xbcb37e8b3f1b09f6),
    ],
    [
        (0xbc62a747ca07d630, 0x3fed6d42e652ce9a),
        (0xbc789f5a03143863, 0x3fd59b462a4134b2),
        (0xbc36139452148f43, 0xbf9309a084e7d879),
        (0xbbede9bf011d0122, 0x3f51e47ac9c4c1e3),
        (0x3bae3a191b4e3711, 0xbf0a468a447d21ea),
        (0x3b516b9dbf20d3a0, 0x3ebccfa848c16ecb),
        (0xbaf45f67850622dc, 0xbe671406d6247e7e),
        (0xba9afce70816748e, 0x3e0a3815485d6074),
        (0x3a4365c1867e0cf7, 0xbda405987f7f2f4b),
        (0x39d30563667171d7, 0x3d3272e30e95ed90),
        (0xb91280c86c884580, 0xbcaf073402f44315),
    ],
    [
        (0x3c8f60a249f7c00e, 0x3fedc740fcccedd7),
        (0x3c53f9df06bc8f9c, 0x3fd559f80c631fe7),
        (0xbc31921248d74572, 0xbf925f03faf7b7d2),
        (0x3bdfe8b708962ff8, 0x3f50dc559c122c5c),
        (0xbba1d03d8e55ebc1, 0xbf082dc34fb7663d),
        (0x3b587dd0630cd995, 0x3eb9e3a65f1e1ccc),
        (0xbad1b315f72bea20, 0xbe644022ea43612d),
        (0x3a92aa9f91588038, 0x3e06774a0eae4e26),
        (0x3a2dde6ed80a8ad4, 0xbda0c0b1b147b2e0),
        (0x39b72f1e01edcf12, 0x3d2e25bd83b43837),
        (0xb915c51aee817f28, 0xbca8c18518a470b6),
    ],
    [
        (0x3c6066aa803f0eb0, 0x3fee21523413f6d4),
        (0x3c701a65181dd95a, 0x3fd51a2372016c24),
        (0x3becd2eeb19f4fa0, 0xbf91bc285adfbae2),
        (0x3bd585c64e7b0238, 0x3f4fcc2f1ab1d691),
        (0xbb937747d5ec3df8, 0xbf064512bf089bca),
        (0x3b5b3a729384d857, 0x3eb74a95ddbb9ed7),
        (0xbb04bce0c7a6c35e, 0xbe61cb92c772ae76),
        (0xba9bc777b30f579a, 0x3e03488a2c937069),
        (0x3a2eef4771938cfe, 0xbd9c17387c41e64a),
        (0xb9ba789ead7c145e, 0x3d28b025d52dcbff),
        (0xb9471fb6ef94b8de, 0xbca3cd451511437b),
    ],
    [
        (0x3c6fdcfd2ad6b2cc, 0x3fee7b70600bc584),
        (0xbc216caa13b9e460, 0x3fd4dbbfb210e2e8),
        (0x3c339b6e95789745, 0xbf9120a815b6c918),
        (0x3b956397b544cce0, 0x3f4e00d1e8922c76),
        (0x3ba4c65063f6319c, 0xbf0487ca2ab8e00b),
        (0x3b5b594e90f0637d, 0x3eb4fa9b5402f99a),
        (0xbabb01e0da08d320, 0xbe5f520c220f27b0),
        (0xbaa38014f8475a9c, 0x3e00947b1d1c07d5),
        (0xba3a70f466ff0512, 0xbd979905fceffdcd),
        (0x39aec257742e626c, 0x3d24434adc2f738f),
        (0xb92109b402248df6, 0xbc9fc2116c6f4f4c),
    ],
    [
        (0xbc8ed7b55bc9a299, 0x3feed5973870ea62),
        (0x3c7068e6a0c0c082, 0x3fd49ec32763cc12),
        (0xbc3079ab6b76d441, 0xbf908c2099da4782),
        (0xbbeea4f5224b5d84, 0x3f4c5414cbe78b75),
        (0x3bac8ba9ee3c50e7, 0xbf02f1b182c9dcaf),
        (0xbb594f6e7ccb3656, 0x3eb2eb11438a7ca9),
        (0xbacdeb584cff4340, 0xbe5b9a34dc857c26),
        (0xba805fa93f84a21c, 0x3dfc8f43f4c51beb),
        (0xba3ae305c497455f, 0xbd93dcbcbc79e194),
        (0x39c91204c96816ba, 0x3d20aaf5b3fed175),
        (0x3931bf2dad1b074d, 0xbc9987b162a8d125),
    ],
    [
        (0xbc8708c57fc49fa0, 0x3fef2fc3ce35d863),
        (0x3c6b3c877a15c102, 0x3fd46323a69e9f48),
        (0xbc27369c4763b491, 0xbf8ffc669e0ee421),
        (0x3bef1f26de28a2cd, 0x3f4ac3a8e2298377),
        (0xbba1cae3482f37ad, 0xbf017efdb93d4bc3),
        (0x3b53791a286e42a2, 0x3eb114642afe2ad3),
        (0xbafcada319b6cbb6, 0xbe585c28eac84be9),
        (0x3a4204182a290740, 0x3df8a37a4be247cb),
        (0x3a1aec8200b2b59c, 0xbd90c016dbd0389b),
        (0xb9bcbc705e49bce8, 0x3d1b7b30ce88ec83),
        (0xb90e04b1b0d7a938, 0xbc9492d96e10325b),
    ],
    [
        (0xbc5a1c7d0cbb1620, 0x3fef89f42525e2f5),
        (0xbc6820327b9fb348, 0x3fd428d6d02b7336),
        (0xbc2028945818c390, 0xbf8eed0c4104b3e1),
        (0xbbeb1e19744aaa74, 0x3f494d6d68346b7e),
        (0xbb8648aa3d83ead0, 0xbf002c46ff7034db),
        (0x3b45bd818ecdcdba, 0x3eaedfe28b22d4e0),
        (0xbacb470408632410, 0xbe5587433a8ae1af),
        (0xba84cce387f694ea, 0x3df54a716368ebb1),
        (0xba16fd37fa555ba4, 0xbd8c4e3a86a2428b),
        (0xb9b5bae13524103e, 0x3d16b4243fb6f92d),
        (0x391f2bc487b07970, 0xbc909e8be69a15eb),
    ],
    [
        (0x3c86cbe5e98a98ab, 0x3fefe426e98d02ad),
        (0xbc7374332a339b7b, 0x3fd3efd247baee74),
        (0x3c1e64f9511446c0, 0xbf8de98772761246),
        (0x3bebc8cddaed336e, 0x3f47ef6d292b758c),
        (0x3b890892e5c34bdc, 0xbefdecfe560cf884),
        (0x3b46edd1273601a7, 0x3eabefd0f34b6491),
        (0xbafabe6880484076, 0xbe530d455c33b91b),
        (0x3a87b53325d0c678, 0x3df26d73fda0c451),
        (0xba2145ca4055c756, 0xbd87f5ea8424c217),
        (0x3970bcc9a5266510, 0x3d12cbd951992e7f),
        (0xb92875f59f8743e5, 0xbc8ae9d6bb861ef8),
    ],
    [
        (0x3c8e56531a4c0964, 0x3ff01f2d9d896b96),
        (0x3c69dd28e00eeaea, 0x3fd3b80bd8b693ad),
        (0x3c2112b49c2d929d, 0xbf8cf13718435314),
        (0xbbd3e3f549a6c02a, 0x3f46a7db8fd4d886),
        (0xbb9cfaf7080719dc, 0xbefbb5d132483335),
        (0x3b129df2d8378b30, 0x3ea94e632358a780),
        (0x3af34f526a85aadc, 0xbe50e1fbc80213d2),
        (0x3a85db7b76383a49, 0x3deff2fc81c56fd6),
        (0x3a1b4963ac2d4f62, 0xbd8451d234f7b2ee),
        (0x3985ca3f55e40518, 0x3d0f2fe7398a45f0),
        (0x392021e0641a748a, 0xbc85d7a01c5f7eb1),
    ],
    [
        (0x3c8d688d52eeb63c, 0x3ff04c4843a795cb),
        (0x3c2e29d7b8b68640, 0x3fd381798d3b7124),
        (0x3c113b1fae95b222, 0xbf8c038376b558a7),
        (0x3bed5a3bd9d8951c, 0x3f457511992ea31d),
        (0x3b7acaf014e5fd04, 0xbef9ae1b7af2711a),
        (0x3b38fcf24e4c4314, 0x3ea6f2a944764535),
        (0xbab02dd93f02bfe0, 0xbe4df5df7475d1b8),
        (0x3a7be4558e764b58, 0x3debbd3b73f426e4),
        (0x39f60932f017fc58, 0xbd814340b64a12fa),
        (0x39962f7e531d98b0, 0x3d09ecf0c3cdff1f),
        (0xb92d928723f3b280, 0xbc81c44f3088b25e),
    ],
    [
        (0x3c75eee764574b40, 0x3ff0796337eb156b),
        (0xbc75feae40a1a90b, 0x3fd34c11bbbceb70),
        (0x3c178be5b54d01d6, 0xbf8b1fddd6af094f),
        (0x3bd64edc5974df88, 0x3f44558acfb2b08c),
        (0x3b946505515a12bb, 0xbef7d172dfd1900f),
        (0x3b287c83bbb858b0, 0x3ea4d4cac4417e94),
        (0xbae9e442fc4b2618, 0xbe4a9e49b7c94308),
        (0xba566f889cc2e640, 0x3de81eda24ccecac),
        (0xba05ed5e30af5d38, 0xbd7d61fb394a66ad),
        (0xb9a9d5b973f44a13, 0x3d05982d519e12cc),
        (0xb906ddcc141d26be, 0xbc7cf7be237827b9),
    ],
    [
        (0xbc81b90566f6f908, 0x3ff0a67e5c3c200c),
        (0xbc7d5212fc82f031, 0x3fd317cb0e502e4c),
        (0x3c200bb08e842505, 0xbf8a45c0157745d2),
        (0xbbebf591fc8f8179, 0x3f4347e266dfc96f),
        (0xbb86d2b6b1fc969e, 0xbef61bdff626f11b),
        (0xbb4b30acc251a2d5, 0x3ea2ede2579e5ca9),
        (0xbabdf54fda20eff0, 0xbe47adc218497f29),
        (0x3a64b88f981d6108, 0x3de5014d76da32ed),
        (0xba0cf8965161f6a2, 0xbd790c89e7a51571),
        (0x397940e2585c8c10, 0x3d020598950e90e1),
        (0xb8fe7525e1f6db28, 0xbc77aa994d491ad0),
    ],
    [
        (0x3c8c4c890adae8f4, 0x3ff0d3999da52293),
        (0xbc6b205b14d29e54, 0x3fd2e49c85c0476f),
        (0xbc1fef66c53ee65e, 0xbf8974ac29e86d4f),
        (0xbbc62f38b0b4df28, 0x3f424ad083d71fe1),
        (0xbb945e74cd665950, 0xbef489d1c88dc8ce),
        (0x3b4aa3a0566b6933, 0x3ea137deb7d59680),
        (0x3ae507d700308bfb, 0xbe4516f993433b0f),
        (0x3a63c8fe3c89e8ac, 0x3de2519519e74a92),
        (0xba130f708fc4a0b1, 0xbd7563ea5df792c4),
        (0xb976d5e23edcbf48, 0x3cfe234f6246180b),
        (0xb8f27fdcff9e8dc4, 0xbc73605c0a952524),
    ],
];