160206(2)

Ruby


原始的アイゼンシュタイン三角形と原始的タレース三角形(2)

辺の長さがいずれも5000 以下の原始的アイゼンシュタイン三角形と原始的タレース三角形を
求めてみた。

class Array
  def gcd
    self.inject{|a, b| a.gcd(b)}
  end
end

n = 5000
# 定理を用いない方法
ary1 = []
(1..n).each{|x|
  (x..n).each{|y|
    m1 = x * x + y * y + x * y
    z = Math.sqrt(m1).to_i
    # x < z, y < z
    if z <= n && z * z == m1 && x + y > z
      ary1 << [x, y, z] if [x, y, z].gcd == 1
    end
  }
}
ary1.sort!

k = 70
# 定理を用いる方法
ary2 = []
(2..k).each{|i|
  (1..i - 1).each{|j|
    if i.gcd(j) == 1 && (i - j) % 3 > 0
      x, y, z = i * i - j * j, 2 * i * j + j * j, i * i + i * j + j * j
      # x < z, y < z
      if z <= n
        ary2 << [x, y, z].sort
      end
    end
  }
}
p ary2.sort!
# 一致の確認
p ary1 == ary2

# 定理を用いない方法
ary3 = []
(1..n).each{|x|
  (x..n).each{|y|
    m2 = x * x + y * y - x * y
    z = Math.sqrt(m2).to_i
    if z <= n && z * z == m2 && x + y > z && y + z > x && z + x > y
      ary3 << [x, y, z].sort if [x, y, z].gcd == 1
    end
  }
}
ary3.sort!

# 定理を用いる方法
ary4 = [[1, 1, 1]]
(2..k).each{|i|
  (1..i - 1).each{|j|
    if i.gcd(j) == 1 && (i - j) % 3 > 0
      u, v, w = i * i - j * j, 2 * i * j + j * j, i * i + i * j + j * j
      # 原始的アイゼンシュタイン三角形を用いて原始的タレース三角形を作る
      x, y, z = u, u + v, w
      if [y, z].max <= n
        ary4 << [x, y, z].sort
      end
      x, y = u + v, v
      if [x, z].max <= n
        ary4 << [x, y, z].sort
      end
    end
  }
}
p ary4.sort!
# 一致の確認
p ary3 == ary4

出力結果
[[3, 5, 7], [5, 16, 19], [7, 8, 13], [7, 33, 37], [9, 56, 61], [11, 24, 31], [11, 85, 91], [13, 35, 43], [13, 120, 127], [15, 161, 169], [16, 39, 49], [17, 63, 73], [17, 208, 217], [19, 80, 91], [19, 261, 271], [21, 320, 331], [23, 120, 133], [23, 385, 397], [24, 95, 109], [25, 143, 157], [25, 456, 469], [27, 533, 547], [29, 195, 211], [29, 616, 631], [31, 224, 241], [31, 705, 721], [32, 45, 67], [32, 175, 193], [33, 800, 817], [35, 288, 307], [35, 901, 919], [37, 323, 343], [37, 1008, 1027], [39, 1121, 1141], [40, 51, 79], [40, 77, 103], [40, 279, 301], [41, 399, 421], [41, 1240, 1261], [43, 440, 463], [43, 1365, 1387], [45, 1496, 1519], [47, 528, 553], [47, 1633, 1657], [48, 407, 433], [49, 575, 601], [49, 1776, 1801], [51, 1925, 1951], [53, 675, 703], [53, 2080, 2107], [55, 57, 97], [55, 728, 757], [55, 2241, 2269], [56, 115, 151], [56, 165, 199], [56, 559, 589], [57, 2408, 2437], [59, 840, 871], [59, 2581, 2611], [61, 899, 931], [61, 2760, 2791], [63, 2945, 2977], [64, 221, 259], [64, 735, 769], [65, 88, 133], [65, 1023, 1057], [65, 3136, 3169], [67, 1088, 1123], [67, 3333, 3367], [69, 91, 139], [69, 3536, 3571], [71, 1224, 1261], [71, 3745, 3781], [72, 203, 247], [72, 935, 973], [73, 1295, 1333], [73, 3960, 3997], [75, 112, 163], [75, 4181, 4219], [77, 1443, 1483], [77, 4408, 4447], [79, 1520, 1561], [79, 4641, 4681], [80, 357, 403], [80, 1159, 1201], [81, 4880, 4921], [83, 1680, 1723], [85, 168, 223], [85, 1763, 1807], [87, 160, 217], [88, 315, 367], [88, 437, 487], [88, 1407, 1453], [89, 1935, 1981], [91, 2024, 2071], [93, 187, 247], [95, 217, 277], [95, 2208, 2257], [96, 1679, 1729], [97, 2303, 2353], [101, 2499, 2551], [103, 2600, 2653], [104, 105, 181], [104, 451, 511], [104, 621, 679], [104, 1975, 2029], [105, 247, 313], [105, 272, 337], [107, 2808, 2863], [109, 2915, 2971], [111, 280, 349], [112, 725, 787], [112, 2295, 2353], [113, 3135, 3193], [115, 333, 403], [115, 3248, 3307], [119, 145, 229], [119, 3480, 3541], [120, 611, 679], [120, 2639, 2701], [121, 3599, 3661], [123, 352, 427], [125, 3843, 3907], [127, 3968, 4033], [128, 957, 1027], [128, 3007, 3073], [129, 391, 469], [131, 4224, 4291], [133, 192, 283], [133, 4355, 4423], [135, 473, 553], [136, 209, 301], [136, 795, 871], [136, 1085, 1159], [136, 3399, 3469], [137, 4623, 4693], [139, 4760, 4831], [141, 475, 559], [144, 155, 259], [144, 3815, 3889], [145, 552, 637], [147, 520, 607], [152, 273, 373], [152, 1003, 1087], [152, 1365, 1447], [152, 4255, 4333], [155, 637, 727], [159, 616, 709], [160, 1517, 1603], [160, 4719, 4801], [161, 304, 409], [165, 667, 763], [165, 728, 823], [168, 1235, 1327], [175, 369, 481], [176, 259, 379], [176, 1845, 1939], [177, 775, 877], [183, 832, 937], [184, 425, 541], [184, 1491, 1591], [184, 2021, 2119], [185, 231, 361], [185, 928, 1033], [189, 440, 559], [195, 952, 1063], [195, 1037, 1147], [200, 513, 637], [200, 1771, 1879], [200, 2397, 2503], [201, 1015, 1129], [203, 517, 643], [205, 299, 439], [205, 1152, 1267], [208, 387, 523], [208, 2597, 2707], [213, 1147, 1267], [215, 336, 481], [215, 1273, 1393], [216, 2075, 2191], [217, 600, 733], [219, 1216, 1339], [224, 3021, 3139], [231, 689, 829], [231, 1360, 1489], [232, 713, 853], [232, 2403, 2527], [232, 3245, 3367], [235, 416, 571], [235, 1533, 1663], [237, 1435, 1567], [240, 253, 427], [240, 287, 457], [240, 539, 691], [245, 459, 619], [245, 1672, 1807], [248, 825, 973], [248, 2755, 2887], [248, 3717, 3847], [249, 1591, 1729], [255, 1672, 1813], [255, 1817, 1957], [256, 3965, 4099], [259, 885, 1039], [264, 325, 511], [264, 3131, 3271], [265, 551, 721], [265, 1968, 2113], [267, 1840, 1987], [272, 715, 883], [272, 4485, 4627], [273, 992, 1153], [273, 1927, 2077], [275, 301, 499], [280, 423, 613], [280, 1073, 1237], [280, 3531, 3679], [280, 4757, 4903], [285, 2107, 2263], [285, 2288, 2443], [287, 1105, 1273], [291, 2200, 2359], [295, 704, 889], [295, 2457, 2617], [296, 1209, 1381], [296, 3955, 4111], [297, 368, 577], [301, 1224, 1399], [303, 2392, 2557], [304, 915, 1099], [305, 759, 949], [305, 2632, 2797], [309, 2491, 2659], [312, 493, 703], [312, 4403, 4567], [315, 1349, 1531], [315, 2813, 2983], [319, 441, 661], [320, 583, 793], [321, 2695, 2869], [327, 2800, 2977], [328, 1505, 1693], [329, 351, 589], [329, 1480, 1669], [335, 936, 1141], [335, 3193, 3373], [336, 589, 811], [336, 1139, 1339], [339, 3016, 3199], [341, 520, 751], [344, 1665, 1861], [345, 3127, 3313], [345, 3392, 3577], [355, 1064, 1279], [355, 3597, 3787], [357, 1760, 1963], [357, 3355, 3547], [360, 767, 997], [363, 3472, 3667], [365, 1131, 1351], [365, 3808, 4003], [368, 1387, 1603], [371, 480, 739], [371, 1909, 2119], [375, 3712, 3913], [376, 2009, 2221], [377, 400, 673], [381, 3835, 4039], [384, 805, 1051], [385, 527, 793], [385, 696, 949], [385, 1271, 1501], [385, 2064, 2281], [385, 4248, 4453], [392, 2193, 2413], [393, 4087, 4297], [395, 1344, 1579], [395, 4477, 4687], [399, 2225, 2449], [399, 4216, 4429], [400, 1659, 1891], [403, 477, 763], [405, 4712, 4927], [407, 793, 1057], [408, 925, 1183], [411, 4480, 4699], [413, 627, 907], [413, 2392, 2623], [415, 1496, 1741], [417, 4615, 4837], [424, 2585, 2821], [427, 680, 967], [427, 2565, 2803], [429, 560, 859], [429, 896, 1171], [432, 1955, 2203], [440, 1207, 1477], [440, 2793, 3037], [445, 1739, 1999], [448, 495, 817], [451, 1005, 1291], [455, 649, 961], [455, 792, 1093], [455, 1824, 2089], [455, 2929, 3181], [456, 1189, 1471], [464, 561, 889], [464, 2275, 2539], [469, 851, 1159], [469, 3120, 3379], [472, 3233, 3493], [473, 1120, 1417], [480, 1333, 1627], [480, 1463, 1753], [481, 744, 1069], [483, 3317, 3583], [485, 2091, 2371], [488, 3465, 3733], [495, 1241, 1549], [496, 665, 1009], [496, 2619, 2899], [497, 975, 1297], [497, 3520, 3793], [504, 671, 1021], [505, 2279, 2569], [511, 1040, 1369], [511, 3729, 4009], [515, 2376, 2671], [517, 1368, 1687], [520, 1743, 2053], [520, 3953, 4237], [525, 3944, 4231], [528, 1645, 1963], [528, 2987, 3283], [531, 544, 931], [533, 952, 1303], [535, 2576, 2881], [536, 4209, 4501], [539, 1501, 1831], [545, 2679, 2989], [549, 595, 991], [552, 1813, 2143], [553, 1247, 1597], [553, 4392, 4693], [559, 1065, 1429], [560, 871, 1249], [560, 897, 1273], [560, 2047, 2377], [560, 3379, 3691], [561, 1640, 1981], [565, 2891, 3211], [567, 4625, 4933], [581, 1395, 1759], [583, 1785, 2137], [585, 703, 1117], [585, 1184, 1561], [592, 1025, 1417], [592, 3795, 4123], [595, 1472, 1843], [595, 3224, 3559], [600, 2173, 2527], [603, 760, 1183], [605, 3339, 3679], [608, 715, 1147], [611, 1309, 1699], [616, 1095, 1501], [623, 1632, 2017], [624, 2365, 2731], [624, 4235, 4579], [627, 2093, 2467], [629, 640, 1099], [635, 3696, 4051], [637, 1440, 1843], [639, 880, 1321], [640, 2727, 3097], [649, 2256, 2641], [655, 3944, 4309], [656, 1305, 1729], [657, 943, 1393], [663, 737, 1213], [663, 1577, 1993], [665, 1887, 2293], [665, 4071, 4441], [671, 2425, 2821], [672, 923, 1387], [672, 1343, 1777], [672, 2773, 3163], [679, 1976, 2389], [680, 741, 1231], [680, 3103, 3493], [685, 4331, 4711], [688, 1457, 1897], [689, 1720, 2149], [693, 1075, 1543], [693, 2600, 3007], [695, 4464, 4849], [696, 2989, 3391], [697, 840, 1333], [707, 2160, 2587], [711, 1144, 1621], [715, 1869, 2311], [715, 2781, 3199], [720, 3503, 3913], [721, 2255, 2689], [728, 1615, 2077], [731, 949, 1459], [736, 1155, 1651], [737, 2968, 3397], [741, 2024, 2479], [744, 3445, 3871], [747, 1288, 1783], [749, 2451, 2899], [752, 1785, 2257], [759, 3161, 3601], [760, 989, 1519], [760, 3927, 4357], [763, 2552, 3007], [765, 1064, 1591], [765, 1363, 1867], [767, 2185, 2653], [768, 3685, 4123], [779, 781, 1351], [781, 3360, 3811], [784, 1961, 2449], [791, 2760, 3229], [793, 2352, 2833], [799, 1185, 1729], [800, 1411, 1939], [801, 1519, 2041], [803, 840, 1423], [803, 3565, 4027], [805, 2867, 3343], [816, 4189, 4651], [817, 888, 1477], [819, 1600, 2131], [819, 2525, 3019], [825, 3776, 4249], [833, 1312, 1873], [840, 2231, 2749], [840, 4453, 4927], [847, 3200, 3697], [848, 2337, 2857], [855, 1001, 1609], [855, 1768, 2317], [864, 1691, 2251], [869, 1035, 1651], [869, 4216, 4711], [871, 2889, 3409], [873, 1855, 2413], [875, 3432, 3943], [880, 1421, 2011], [880, 2537, 3073], [889, 3551, 4069], [891, 4445, 4951], [893, 1120, 1747], [896, 2575, 3121], [897, 3080, 3613], [901, 1584, 2179], [909, 2035, 2611], [913, 1175, 1813], [917, 3795, 4327], [920, 1027, 1687], [920, 1581, 2191], [923, 3277, 3823], [927, 2128, 2713], [928, 1995, 2587], [931, 1245, 1891], [935, 1248, 1897], [935, 1729, 2341], [944, 2961, 3529], [949, 3480, 4039], [952, 2943, 3517], [959, 4176, 4729], [963, 2320, 2923], [969, 1376, 2041], [969, 1880, 2509], [973, 4307, 4867], [975, 3689, 4261], [976, 3185, 3769], [979, 1400, 2071], [981, 2419, 3031], [984, 1081, 1789], [992, 2323, 2947], [1001, 1479, 2161], [1001, 3904, 4489], [1003, 2037, 2683], [1007, 1513, 2197], [1008, 3335, 3937], [1017, 2623, 3253], [1027, 4125, 4723], [1032, 1225, 1957], [1035, 2728, 3367], [1037, 2200, 2863], [1040, 2109, 2779], [1040, 3657, 4273], [1045, 1643, 2347], [1045, 1656, 2359], [1053, 4352, 4963], [1056, 1079, 1849], [1056, 2675, 3331], [1064, 3751, 4381], [1067, 1728, 2443], [1071, 2369, 3049], [1071, 2944, 3601], [1072, 3905, 4537], [1080, 1547, 2287], [1089, 3055, 3721], [1105, 1127, 1933], [1105, 2544, 3241], [1111, 1904, 2641], [1120, 2501, 3211], [1120, 3051, 3739], [1120, 4191, 4849], [1121, 1960, 2701], [1125, 3283, 3967], [1128, 1537, 2317], [1133, 1995, 2743], [1139, 2725, 3439], [1143, 3400, 4093], [1144, 1335, 2149], [1157, 1275, 2107], [1159, 2121, 2881], [1160, 1843, 2623], [1160, 2709, 3439], [1173, 1232, 2083], [1173, 2912, 3643], [1176, 1705, 2509], [1177, 2183, 2953], [1179, 3640, 4351], [1184, 3451, 4171], [1197, 2288, 3067], [1197, 3763, 4483], [1199, 2280, 3061], [1207, 3105, 3853], [1219, 1365, 2239], [1232, 1615, 2473], [1233, 4015, 4753], [1235, 1512, 2383], [1235, 2461, 3259], [1240, 2163, 2983], [1240, 3149, 3919], [1241, 3304, 4069], [1243, 2480, 3283], [1248, 3875, 4627], [1251, 4144, 4891], [1261, 1595, 2479], [1265, 1504, 2401], [1265, 2583, 3397], [1272, 2065, 2917], [1273, 2640, 3457], [1275, 3509, 4291], [1280, 3381, 4171], [1288, 1325, 2263], [1309, 2795, 3631], [1309, 3720, 4519], [1311, 1649, 2569], [1311, 2825, 3661], [1313, 1767, 2677], [1320, 1919, 2821], [1320, 2257, 3133], [1320, 2507, 3367], [1339, 1856, 2779], [1343, 3937, 4753], [1349, 3016, 3871], [1357, 1800, 2743], [1360, 3869, 4699], [1375, 3128, 3997], [1377, 4160, 4993], [1387, 3213, 4087], [1391, 2040, 2989], [1397, 3243, 4123], [1400, 1653, 2647], [1403, 1957, 2923], [1408, 2247, 3193], [1416, 2665, 3589], [1417, 2135, 3097], [1425, 1568, 2593], [1425, 3416, 4309], [1441, 3479, 4381], [1449, 2120, 3109], [1455, 1456, 2521], [1456, 1829, 2851], [1463, 3600, 4513], [1463, 3625, 4537], [1464, 2881, 3829], [1469, 2331, 3319], [1475, 1717, 2767], [1480, 3267, 4207], [1495, 2289, 3301], [1495, 2432, 3433], [1496, 2599, 3589], [1501, 3840, 4771], [1507, 3848, 4783], [1515, 1624, 2719], [1525, 1872, 2947], [1529, 3975, 4921], [1541, 2464, 3499], [1545, 1711, 2821], [1547, 2640, 3667], [1560, 1751, 2869], [1560, 3337, 4333], [1560, 3683, 4663], [1573, 2747, 3787], [1575, 2033, 3133], [1584, 2975, 4009], [1605, 1891, 3031], [1608, 3577, 4597], [1624, 2405, 3511], [1625, 2967, 4033], [1633, 2832, 3913], [1635, 1984, 3139], [1651, 3080, 4159], [1664, 2071, 3241], [1672, 3375, 4453], [1675, 2373, 3523], [1679, 3025, 4129], [1695, 2176, 3361], [1696, 1769, 3001], [1703, 3312, 4417], [1725, 2552, 3727], [1725, 3224, 4351], [1729, 3431, 4549], [1736, 1819, 3079], [1736, 2829, 3991], [1760, 1953, 3217], [1760, 3799, 4921], [1768, 2415, 3637], [1771, 3429, 4579], [1775, 2737, 3937], [1781, 3675, 4819], [1785, 2479, 3709], [1792, 3053, 4243], [1807, 3800, 4957], [1815, 2584, 3829], [1817, 3640, 4813], [1825, 2928, 4153], [1827, 1853, 3187], [1848, 2147, 3463], [1872, 2783, 4057], [1885, 2016, 3379], [1888, 2345, 3673], [1904, 3525, 4771], [1905, 2911, 4201], [1921, 2015, 3409], [1925, 3328, 4603], [1943, 2185, 3577], [1952, 2553, 3913], [1955, 2112, 3523], [1965, 3139, 4459], [1975, 3537, 4837], [1976, 3175, 4501], [1995, 3256, 4591], [2001, 2360, 3781], [2055, 3496, 4861], [2057, 2415, 3877], [2059, 2541, 3991], [2072, 2875, 4303], [2077, 2088, 3607], [2080, 2993, 4417], [2080, 3591, 4969], [2085, 3619, 4999], [2117, 2728, 4207], [2125, 2627, 4123], [2139, 2261, 3811], [2144, 3225, 4681], [2159, 2736, 4249], [2175, 2921, 4429], [2184, 3275, 4759], [2201, 2440, 4021], [2227, 2960, 4507], [2232, 2485, 4087], [2233, 3120, 4657], [2240, 2299, 3931], [2261, 3075, 4639], [2263, 2625, 4237], [2291, 3325, 4891], [2304, 2701, 4339], [2325, 2816, 4459], [2329, 3311, 4909], [2368, 2667, 4363], [2375, 2448, 4177], [2387, 3013, 4687], [2413, 2555, 4303], [2448, 3157, 4867], [2449, 3216, 4921], [2489, 2775, 4561], [2496, 3059, 4819], [2584, 2751, 4621], [2603, 3120, 4963], [2680, 2849, 4789], [2765, 2992, 4987]]
true
[[1, 1, 1], [3, 7, 8], [5, 7, 8], [5, 19, 21], [7, 13, 15], [7, 37, 40], [8, 13, 15], [9, 61, 65], [11, 31, 35], [11, 91, 96], [13, 43, 48], [13, 127, 133], [15, 169, 176], [16, 19, 21], [16, 49, 55], [17, 73, 80], [17, 217, 225], [19, 91, 99], [19, 271, 280], [21, 331, 341], [23, 133, 143], [23, 397, 408], [24, 31, 35], [24, 109, 119], [25, 157, 168], [25, 469, 481], [27, 547, 560], [29, 211, 224], [29, 631, 645], [31, 241, 255], [31, 721, 736], [32, 67, 77], [32, 193, 207], [33, 37, 40], [33, 817, 833], [35, 43, 48], [35, 307, 323], [35, 919, 936], [37, 343, 360], [37, 1027, 1045], [39, 49, 55], [39, 1141, 1160], [40, 79, 91], [40, 103, 117], [40, 301, 319], [41, 421, 440], [41, 1261, 1281], [43, 463, 483], [43, 1387, 1408], [45, 67, 77], [45, 1519, 1541], [47, 553, 575], [47, 1657, 1680], [48, 433, 455], [49, 601, 624], [49, 1801, 1825], [51, 79, 91], [51, 1951, 1976], [53, 703, 728], [53, 2107, 2133], [55, 97, 112], [55, 757, 783], [55, 2269, 2296], [56, 61, 65], [56, 151, 171], [56, 199, 221], [56, 589, 615], [57, 97, 112], [57, 2437, 2465], [59, 871, 899], [59, 2611, 2640], [61, 931, 960], [61, 2791, 2821], [63, 73, 80], [63, 2977, 3008], [64, 259, 285], [64, 769, 799], [65, 133, 153], [65, 1057, 1088], [65, 3169, 3201], [67, 1123, 1155], [67, 3367, 3400], [69, 139, 160], [69, 3571, 3605], [71, 1261, 1295], [71, 3781, 3816], [72, 247, 275], [72, 973, 1007], [73, 1333, 1368], [73, 3997, 4033], [75, 163, 187], [75, 4219, 4256], [77, 103, 117], [77, 1483, 1520], [77, 4447, 4485], [79, 1561, 1599], [79, 4681, 4720], [80, 91, 99], [80, 403, 437], [80, 1201, 1239], [81, 4921, 4961], [83, 1723, 1763], [85, 91, 96], [85, 223, 253], [85, 1807, 1848], [87, 217, 247], [88, 133, 153], [88, 367, 403], [88, 487, 525], [88, 1453, 1495], [89, 1981, 2024], [91, 139, 160], [91, 2071, 2115], [93, 247, 280], [95, 109, 119], [95, 277, 312], [95, 2257, 2303], [96, 1729, 1775], [97, 2353, 2400], [101, 2551, 2600], [103, 2653, 2703], [104, 181, 209], [104, 511, 555], [104, 679, 725], [104, 2029, 2079], [105, 181, 209], [105, 313, 352], [105, 337, 377], [107, 2863, 2915], [109, 2971, 3024], [111, 349, 391], [112, 163, 187], [112, 787, 837], [112, 2353, 2407], [113, 3193, 3248], [115, 151, 171], [115, 403, 448], [115, 3307, 3363], [119, 229, 264], [119, 3541, 3599], [120, 127, 133], [120, 133, 143], [120, 679, 731], [120, 2701, 2759], [121, 3661, 3720], [123, 427, 475], [125, 3907, 3968], [127, 4033, 4095], [128, 1027, 1085], [128, 3073, 3135], [129, 469, 520], [131, 4291, 4355], [133, 283, 325], [133, 4423, 4488], [135, 553, 608], [136, 301, 345], [136, 871, 931], [136, 1159, 1221], [136, 3469, 3535], [137, 4693, 4760], [139, 4831, 4899], [141, 559, 616], [143, 157, 168], [144, 259, 299], [144, 3889, 3959], [145, 229, 264], [145, 637, 697], [147, 607, 667], [152, 373, 425], [152, 1087, 1155], [152, 1447, 1517], [152, 4333, 4407], [155, 259, 299], [155, 727, 792], [159, 709, 775], [160, 217, 247], [160, 1603, 1677], [160, 4801, 4879], [161, 169, 176], [161, 409, 465], [165, 199, 221], [165, 763, 832], [165, 823, 893], [168, 223, 253], [168, 1327, 1403], [175, 193, 207], [175, 481, 544], [176, 379, 435], [176, 1939, 2021], [177, 877, 952], [183, 937, 1015], [184, 541, 609], [184, 1591, 1675], [184, 2119, 2205], [185, 361, 416], [185, 1033, 1113], [187, 247, 280], [189, 559, 629], [192, 283, 325], [195, 211, 224], [195, 1063, 1147], [195, 1147, 1232], [200, 637, 713], [200, 1879, 1971], [200, 2503, 2597], [201, 1129, 1216], [203, 247, 275], [203, 643, 720], [205, 439, 504], [205, 1267, 1357], [208, 217, 225], [208, 523, 595], [208, 2707, 2805], [209, 301, 345], [213, 1267, 1360], [215, 481, 551], [215, 1393, 1488], [216, 2191, 2291], [217, 277, 312], [217, 733, 817], [219, 1339, 1435], [221, 259, 285], [224, 241, 255], [224, 3139, 3245], [231, 361, 416], [231, 829, 920], [231, 1489, 1591], [232, 853, 945], [232, 2527, 2635], [232, 3367, 3477], [235, 571, 651], [235, 1663, 1768], [237, 1567, 1672], [240, 427, 493], [240, 457, 527], [240, 691, 779], [245, 619, 704], [245, 1807, 1917], [247, 313, 352], [248, 973, 1073], [248, 2887, 3003], [248, 3847, 3965], [249, 1729, 1840], [253, 427, 493], [255, 1813, 1927], [255, 1957, 2072], [256, 4099, 4221], [259, 379, 435], [259, 1039, 1144], [261, 271, 280], [264, 511, 589], [264, 3271, 3395], [265, 721, 816], [265, 2113, 2233], [267, 1987, 2107], [272, 337, 377], [272, 883, 987], [272, 4627, 4757], [273, 373, 425], [273, 1153, 1265], [273, 2077, 2200], [275, 499, 576], [279, 301, 319], [280, 349, 391], [280, 613, 703], [280, 1237, 1353], [280, 3679, 3811], [285, 2263, 2392], [285, 2443, 2573], [287, 457, 527], [287, 1273, 1392], [288, 307, 323], [291, 2359, 2491], [295, 889, 999], [295, 2617, 2752], [296, 1381, 1505], [296, 4111, 4251], [297, 577, 665], [299, 439, 504], [301, 499, 576], [301, 1399, 1525], [303, 2557, 2695], [304, 409, 465], [304, 1099, 1219], [305, 949, 1064], [305, 2797, 2937], [309, 2659, 2800], [312, 703, 805], [312, 4567, 4715], [315, 367, 403], [315, 1531, 1664], [315, 2983, 3128], [319, 661, 760], [320, 331, 341], [320, 793, 903], [321, 2869, 3016], [323, 343, 360], [325, 511, 589], [327, 2977, 3127], [328, 1693, 1833], [329, 589, 680], [329, 1669, 1809], [333, 403, 448], [335, 1141, 1271], [335, 3373, 3528], [336, 481, 551], [336, 811, 925], [336, 1339, 1475], [339, 3199, 3355], [341, 751, 861], [344, 1861, 2009], [345, 3313, 3472], [345, 3577, 3737], [351, 589, 680], [352, 427, 475], [355, 1279, 1419], [355, 3787, 3952], [357, 403, 437], [357, 1963, 2117], [357, 3547, 3712], [360, 997, 1127], [363, 3667, 3835], [365, 1351, 1496], [365, 4003, 4173], [368, 577, 665], [368, 1603, 1755], [369, 481, 544], [371, 739, 851], [371, 2119, 2280], [375, 3913, 4087], [376, 2221, 2385], [377, 673, 777], [381, 4039, 4216], [384, 1051, 1189], [385, 397, 408], [385, 793, 912], [385, 949, 1081], [385, 1501, 1656], [385, 2281, 2449], [385, 4453, 4633], [387, 523, 595], [391, 469, 520], [392, 2413, 2585], [393, 4297, 4480], [395, 1579, 1739], [395, 4687, 4872], [399, 421, 440], [399, 2449, 2624], [399, 4429, 4615], [400, 673, 777], [400, 1891, 2059], [403, 763, 880], [407, 433, 455], [407, 1057, 1200], [408, 1183, 1333], [411, 4699, 4891], [413, 907, 1040], [413, 2623, 2805], [415, 1741, 1911], [416, 571, 651], [423, 613, 703], [424, 2821, 3009], [425, 541, 609], [427, 967, 1107], [427, 2803, 2992], [429, 859, 989], [429, 1171, 1325], [432, 2203, 2387], [437, 487, 525], [440, 463, 483], [440, 559, 629], [440, 1477, 1647], [440, 3037, 3233], [441, 661, 760], [445, 1999, 2184], [448, 817, 943], [451, 511, 555], [451, 1291, 1456], [455, 961, 1104], [455, 1093, 1247], [455, 2089, 2279], [455, 3181, 3384], [456, 469, 481], [456, 1471, 1645], [459, 619, 704], [464, 889, 1025], [464, 2539, 2739], [469, 1159, 1320], [469, 3379, 3589], [472, 3493, 3705], [473, 553, 608], [473, 1417, 1593], [475, 559, 616], [477, 763, 880], [480, 739, 851], [480, 1627, 1813], [480, 1753, 1943], [481, 1069, 1225], [483, 3583, 3800], [485, 2371, 2576], [488, 3733, 3953], [493, 703, 805], [495, 817, 943], [495, 1549, 1736], [496, 1009, 1161], [496, 2899, 3115], [497, 1297, 1472], [497, 3793, 4017], [504, 1021, 1175], [505, 2569, 2784], [511, 1369, 1551], [511, 4009, 4240], [513, 637, 713], [515, 2671, 2891], [517, 643, 720], [517, 1687, 1885], [520, 607, 667], [520, 751, 861], [520, 2053, 2263], [520, 4237, 4473], [525, 4231, 4469], [527, 793, 912], [528, 553, 575], [528, 1963, 2173], [528, 3283, 3515], [531, 931, 1075], [533, 547, 560], [533, 1303, 1485], [535, 2881, 3111], [536, 4501, 4745], [539, 691, 779], [539, 1831, 2040], [544, 931, 1075], [545, 2989, 3224], [549, 991, 1144], [551, 721, 816], [552, 637, 697], [552, 2143, 2365], [553, 1597, 1800], [553, 4693, 4945], [559, 589, 615], [559, 1429, 1624], [560, 859, 989], [560, 1249, 1431], [560, 1273, 1457], [560, 2377, 2607], [560, 3691, 3939], [561, 889, 1025], [561, 1981, 2201], [565, 3211, 3456], [575, 601, 624], [581, 1759, 1976], [583, 793, 903], [583, 2137, 2368], [585, 1117, 1288], [585, 1561, 1769], [589, 811, 925], [592, 1417, 1617], [592, 4123, 4387], [595, 991, 1144], [595, 1843, 2067], [595, 3559, 3819], [600, 733, 817], [600, 2527, 2773], [603, 1183, 1363], [605, 3679, 3944], [608, 1147, 1323], [611, 679, 731], [611, 1699, 1920], [616, 631, 645], [616, 709, 775], [616, 1501, 1711], [621, 679, 725], [623, 2017, 2255], [624, 2731, 2989], [624, 4579, 4859], [627, 907, 1040], [627, 2467, 2720], [629, 1099, 1269], [635, 4051, 4331], [637, 727, 792], [637, 1843, 2077], [639, 1321, 1519], [640, 1099, 1269], [640, 3097, 3367], [649, 961, 1104], [649, 2641, 2905], [655, 4309, 4599], [656, 1729, 1961], [657, 1393, 1600], [663, 1213, 1400], [663, 1993, 2240], [665, 1009, 1161], [665, 2293, 2552], [665, 4441, 4736], [667, 763, 832], [671, 1021, 1175], [671, 2821, 3096], [672, 1387, 1595], [672, 1777, 2015], [672, 3163, 3445], [675, 703, 728], [679, 2389, 2655], [680, 967, 1107], [680, 1231, 1421], [680, 3493, 3783], [688, 1897, 2145], [689, 829, 920], [689, 2149, 2409], [693, 1543, 1768], [693, 3007, 3293], [696, 949, 1081], [696, 3391, 3685], [697, 1333, 1537], [703, 1117, 1288], [704, 889, 999], [705, 721, 736], [707, 2587, 2867], [711, 1621, 1855], [713, 853, 945], [715, 883, 987], [715, 1147, 1323], [715, 2311, 2584], [715, 3199, 3496], [720, 3913, 4223], [721, 2689, 2976], [725, 787, 837], [728, 757, 783], [728, 823, 893], [728, 2077, 2343], [731, 1459, 1680], [735, 769, 799], [736, 1651, 1891], [737, 1213, 1400], [737, 3397, 3705], [741, 1231, 1421], [741, 2479, 2765], [744, 1069, 1225], [744, 3871, 4189], [747, 1783, 2035], [749, 2899, 3200], [752, 2257, 2537], [759, 949, 1064], [759, 3601, 3920], [760, 1183, 1363], [760, 1519, 1749], [760, 4357, 4687], [763, 3007, 3315], [765, 1591, 1829], [765, 1867, 2128], [767, 997, 1127], [767, 2653, 2952], [768, 4123, 4453], [775, 877, 952], [779, 1351, 1560], [781, 1351, 1560], [781, 3811, 4141], [784, 2449, 2745], [791, 3229, 3551], [792, 1093, 1247], [793, 1057, 1200], [793, 2833, 3145], [795, 871, 931], [799, 1729, 1984], [800, 817, 833], [800, 1939, 2211], [801, 2041, 2320], [803, 1423, 1643], [803, 4027, 4368], [805, 1051, 1189], [805, 3343, 3672], [817, 1477, 1705], [819, 2131, 2419], [819, 3019, 3344], [825, 973, 1073], [825, 4249, 4601], [832, 937, 1015], [833, 1873, 2145], [840, 871, 899], [840, 1333, 1537], [840, 1423, 1643], [840, 2749, 3071], [847, 3697, 4047], [848, 2857, 3185], [851, 1159, 1320], [855, 1609, 1856], [855, 2317, 2623], [864, 2251, 2555], [869, 1651, 1904], [871, 1249, 1431], [871, 3409, 3760], [873, 2413, 2728], [875, 3943, 4307], [880, 1321, 1519], [880, 2011, 2301], [880, 3073, 3417], [885, 1039, 1144], [888, 1477, 1705], [889, 4069, 4440], [893, 1747, 2013], [896, 1171, 1325], [896, 3121, 3471], [897, 1273, 1457], [897, 3613, 3977], [899, 931, 960], [901, 919, 936], [901, 2179, 2485], [909, 2611, 2944], [913, 1813, 2088], [915, 1099, 1219], [917, 4327, 4712], [920, 1687, 1947], [920, 2191, 2501], [923, 1387, 1595], [923, 3823, 4200], [925, 1183, 1333], [927, 2713, 3055], [928, 1033, 1113], [928, 2587, 2923], [931, 1891, 2176], [935, 973, 1007], [935, 1897, 2183], [935, 2341, 2664], [936, 1141, 1271], [943, 1393, 1600], [944, 3529, 3905], [949, 1459, 1680], [949, 4039, 4429], [952, 1063, 1147], [952, 1303, 1485], [952, 3517, 3895], [957, 1027, 1085], [963, 2923, 3283], [969, 2041, 2345], [969, 2509, 2849], [975, 1297, 1472], [975, 4261, 4664], [976, 3769, 4161], [979, 2071, 2379], [981, 3031, 3400], [984, 1789, 2065], [989, 1519, 1749], [992, 1153, 1265], [992, 2947, 3315], [1001, 1609, 1856], [1001, 2161, 2480], [1001, 4489, 4905], [1003, 1087, 1155], [1003, 2683, 3040], [1005, 1291, 1456], [1007, 2197, 2520], [1008, 1027, 1045], [1008, 3937, 4343], [1015, 1129, 1216], [1017, 3253, 3640], [1023, 1057, 1088], [1025, 1417, 1617], [1027, 1687, 1947], [1032, 1957, 2257], [1035, 1651, 1904], [1035, 3367, 3763], [1037, 1147, 1232], [1037, 2863, 3237], [1040, 1369, 1551], [1040, 2779, 3149], [1040, 4273, 4697], [1045, 2347, 2688], [1045, 2359, 2701], [1056, 1849, 2135], [1056, 3331, 3731], [1064, 1279, 1419], [1064, 1591, 1829], [1064, 4381, 4815], [1065, 1429, 1624], [1067, 2443, 2795], [1071, 3049, 3440], [1071, 3601, 4015], [1072, 4537, 4977], [1073, 1237, 1353], [1075, 1543, 1768], [1079, 1849, 2135], [1080, 2287, 2627], [1081, 1789, 2065], [1085, 1159, 1221], [1088, 1123, 1155], [1089, 3721, 4144], [1095, 1501, 1711], [1105, 1273, 1392], [1105, 1933, 2232], [1105, 3241, 3649], [1111, 2641, 3015], [1120, 1417, 1593], [1120, 1747, 2013], [1120, 3211, 3621], [1120, 3739, 4171], [1121, 1141, 1160], [1121, 2701, 3081], [1125, 3967, 4408], [1127, 1933, 2232], [1128, 2317, 2665], [1131, 1351, 1496], [1133, 2743, 3128], [1139, 1339, 1475], [1139, 3439, 3864], [1143, 4093, 4543], [1144, 1621, 1855], [1144, 2149, 2479], [1147, 1267, 1360], [1152, 1267, 1357], [1155, 1651, 1891], [1157, 2107, 2432], [1159, 1201, 1239], [1159, 2881, 3280], [1160, 2623, 3003], [1160, 3439, 3869], [1173, 2083, 2405], [1173, 3643, 4085], [1175, 1813, 2088], [1176, 2509, 2881], [1177, 2953, 3360], [1179, 4351, 4819], [1184, 1561, 1769], [1184, 4171, 4635], [1185, 1729, 1984], [1189, 1471, 1645], [1197, 3067, 3485], [1197, 4483, 4960], [1199, 3061, 3479], [1207, 1477, 1647], [1207, 3853, 4312], [1209, 1381, 1505], [1216, 1339, 1435], [1219, 2239, 2584], [1224, 1261, 1295], [1224, 1399, 1525], [1225, 1957, 2257], [1232, 2083, 2405], [1232, 2473, 2847], [1235, 1327, 1403], [1235, 2383, 2747], [1235, 3259, 3696], [1240, 1261, 1281], [1240, 2983, 3403], [1240, 3919, 4389], [1241, 1549, 1736], [1241, 4069, 4545], [1243, 3283, 3723], [1245, 1891, 2176], [1247, 1597, 1800], [1248, 1897, 2183], [1261, 2479, 2856], [1265, 2401, 2769], [1265, 3397, 3848], [1271, 1501, 1656], [1272, 2917, 3337], [1273, 1393, 1488], [1273, 3457, 3913], [1275, 2107, 2432], [1275, 4291, 4784], [1280, 4171, 4661], [1288, 1783, 2035], [1288, 2263, 2613], [1295, 1333, 1368], [1305, 1729, 1961], [1309, 1699, 1920], [1309, 3631, 4104], [1311, 2569, 2960], [1311, 3661, 4136], [1312, 1873, 2145], [1313, 2677, 3080], [1320, 2821, 3239], [1320, 3133, 3577], [1320, 3367, 3827], [1325, 2263, 2613], [1333, 1627, 1813], [1335, 2149, 2479], [1339, 2779, 3195], [1343, 1777, 2015], [1344, 1579, 1739], [1349, 1531, 1664], [1349, 3871, 4365], [1357, 2743, 3157], [1360, 1489, 1591], [1363, 1867, 2128], [1365, 1387, 1408], [1365, 1447, 1517], [1365, 2239, 2584], [1368, 1687, 1885], [1375, 3997, 4503], [1376, 2041, 2345], [1387, 1603, 1755], [1387, 4087, 4600], [1391, 2989, 3431], [1395, 1759, 1976], [1397, 4123, 4640], [1400, 2071, 2379], [1400, 2647, 3053], [1403, 2923, 3360], [1407, 1453, 1495], [1408, 3193, 3655], [1411, 1939, 2211], [1416, 3589, 4081], [1417, 3097, 3552], [1421, 2011, 2301], [1425, 2593, 2993], [1425, 4309, 4841], [1435, 1567, 1672], [1440, 1843, 2077], [1441, 4381, 4920], [1443, 1483, 1520], [1449, 3109, 3569], [1455, 2521, 2911], [1456, 2521, 2911], [1456, 2851, 3285], [1457, 1897, 2145], [1463, 1753, 1943], [1464, 3829, 4345], [1469, 3319, 3800], [1472, 1843, 2067], [1475, 2767, 3192], [1479, 2161, 2480], [1480, 1669, 1809], [1480, 4207, 4747], [1491, 1591, 1675], [1495, 3301, 3784], [1495, 3433, 3927], [1496, 1519, 1541], [1496, 1741, 1911], [1496, 3589, 4095], [1501, 1831, 2040], [1504, 2401, 2769], [1505, 1693, 1833], [1512, 2383, 2747], [1513, 2197, 2520], [1515, 2719, 3139], [1517, 1603, 1677], [1519, 2041, 2320], [1520, 1561, 1599], [1525, 2947, 3397], [1533, 1663, 1768], [1537, 2317, 2665], [1541, 3499, 4005], [1545, 2821, 3256], [1547, 2287, 2627], [1547, 3667, 4187], [1560, 2869, 3311], [1560, 4333, 4897], [1568, 2593, 2993], [1573, 3787, 4320], [1575, 3133, 3608], [1577, 1993, 2240], [1581, 2191, 2501], [1584, 2179, 2485], [1584, 4009, 4559], [1591, 1729, 1840], [1595, 2479, 2856], [1600, 2131, 2419], [1605, 3031, 3496], [1615, 2077, 2343], [1615, 2473, 2847], [1624, 2719, 3139], [1624, 3511, 4029], [1625, 4033, 4592], [1632, 2017, 2255], [1633, 1657, 1680], [1633, 3913, 4465], [1635, 3139, 3619], [1640, 1981, 2201], [1643, 2347, 2688], [1645, 1963, 2173], [1649, 2569, 2960], [1651, 4159, 4731], [1653, 2647, 3053], [1656, 2359, 2701], [1659, 1891, 2059], [1664, 3241, 3735], [1665, 1861, 2009], [1672, 1807, 1917], [1672, 1813, 1927], [1675, 3523, 4048], [1679, 1729, 1775], [1679, 4129, 4704], [1680, 1723, 1763], [1691, 2251, 2555], [1695, 3361, 3871], [1696, 3001, 3465], [1705, 2509, 2881], [1711, 2821, 3256], [1717, 2767, 3192], [1720, 2149, 2409], [1725, 3727, 4277], [1725, 4351, 4949], [1728, 2443, 2795], [1729, 2341, 2664], [1736, 3079, 3555], [1736, 3991, 4565], [1739, 1999, 2184], [1743, 2053, 2263], [1751, 2869, 3311], [1760, 1963, 2117], [1760, 3217, 3713], [1763, 1807, 1848], [1767, 2677, 3080], [1768, 2317, 2623], [1768, 3637, 4183], [1769, 3001, 3465], [1771, 1879, 1971], [1775, 3937, 4512], [1776, 1801, 1825], [1785, 2137, 2368], [1785, 2257, 2537], [1785, 3709, 4264], [1792, 4243, 4845], [1800, 2743, 3157], [1813, 2143, 2365], [1815, 3829, 4399], [1817, 1957, 2072], [1819, 3079, 3555], [1824, 2089, 2279], [1825, 4153, 4753], [1827, 3187, 3680], [1829, 2851, 3285], [1840, 1987, 2107], [1843, 2623, 3003], [1845, 1939, 2021], [1848, 3463, 3995], [1853, 3187, 3680], [1855, 2413, 2728], [1856, 2779, 3195], [1869, 2311, 2584], [1872, 2947, 3397], [1872, 4057, 4655], [1880, 2509, 2849], [1885, 3379, 3901], [1887, 2293, 2552], [1888, 3673, 4233], [1891, 3031, 3496], [1904, 2641, 3015], [1905, 4201, 4816], [1909, 2119, 2280], [1919, 2821, 3239], [1921, 3409, 3936], [1925, 1951, 1976], [1927, 2077, 2200], [1935, 1981, 2024], [1943, 3577, 4128], [1952, 3913, 4505], [1953, 3217, 3713], [1955, 2203, 2387], [1955, 3523, 4067], [1957, 2923, 3360], [1960, 2701, 3081], [1961, 2449, 2745], [1968, 2113, 2233], [1975, 2029, 2079], [1976, 2389, 2655], [1984, 3139, 3619], [1995, 2587, 2923], [1995, 2743, 3128], [2001, 3781, 4361], [2009, 2221, 2385], [2015, 3409, 3936], [2016, 3379, 3901], [2021, 2119, 2205], [2024, 2071, 2115], [2024, 2479, 2765], [2033, 3133, 3608], [2035, 2611, 2944], [2037, 2683, 3040], [2040, 2989, 3431], [2047, 2377, 2607], [2057, 3877, 4472], [2059, 3991, 4600], [2064, 2281, 2449], [2065, 2917, 3337], [2071, 3241, 3735], [2072, 4303, 4947], [2075, 2191, 2291], [2077, 3607, 4165], [2080, 2107, 2133], [2088, 3607, 4165], [2091, 2371, 2576], [2093, 2467, 2720], [2107, 2263, 2392], [2109, 2779, 3149], [2112, 3523, 4067], [2117, 4207, 4845], [2120, 3109, 3569], [2121, 2881, 3280], [2125, 4123, 4752], [2128, 2713, 3055], [2135, 3097, 3552], [2139, 3811, 4400], [2147, 3463, 3995], [2159, 4249, 4895], [2160, 2587, 2867], [2163, 2983, 3403], [2173, 2527, 2773], [2176, 3361, 3871], [2183, 2953, 3360], [2185, 2653, 2952], [2185, 3577, 4128], [2193, 2413, 2585], [2200, 2359, 2491], [2200, 2863, 3237], [2201, 4021, 4641], [2208, 2257, 2303], [2225, 2449, 2624], [2231, 2749, 3071], [2232, 4087, 4717], [2240, 3931, 4539], [2241, 2269, 2296], [2247, 3193, 3655], [2255, 2689, 2976], [2256, 2641, 2905], [2257, 3133, 3577], [2261, 3811, 4400], [2263, 4237, 4888], [2275, 2539, 2739], [2279, 2569, 2784], [2280, 3061, 3479], [2288, 2443, 2573], [2288, 3067, 3485], [2289, 3301, 3784], [2295, 2353, 2407], [2299, 3931, 4539], [2303, 2353, 2400], [2320, 2923, 3283], [2323, 2947, 3315], [2331, 3319, 3800], [2337, 2857, 3185], [2345, 3673, 4233], [2352, 2833, 3145], [2360, 3781, 4361], [2365, 2731, 2989], [2369, 3049, 3440], [2373, 3523, 4048], [2375, 4177, 4823], [2376, 2671, 2891], [2392, 2557, 2695], [2392, 2623, 2805], [2397, 2503, 2597], [2403, 2527, 2635], [2405, 3511, 4029], [2408, 2437, 2465], [2413, 4303, 4968], [2415, 3637, 4183], [2415, 3877, 4472], [2419, 3031, 3400], [2425, 2821, 3096], [2432, 3433, 3927], [2440, 4021, 4641], [2448, 4177, 4823], [2451, 2899, 3200], [2457, 2617, 2752], [2461, 3259, 3696], [2464, 3499, 4005], [2479, 3709, 4264], [2480, 3283, 3723], [2485, 4087, 4717], [2491, 2659, 2800], [2499, 2551, 2600], [2501, 3211, 3621], [2507, 3367, 3827], [2525, 3019, 3344], [2537, 3073, 3417], [2541, 3991, 4600], [2544, 3241, 3649], [2552, 3007, 3315], [2552, 3727, 4277], [2553, 3913, 4505], [2555, 4303, 4968], [2565, 2803, 2992], [2575, 3121, 3471], [2576, 2881, 3111], [2581, 2611, 2640], [2583, 3397, 3848], [2584, 3829, 4399], [2585, 2821, 3009], [2597, 2707, 2805], [2599, 3589, 4095], [2600, 2653, 2703], [2600, 3007, 3293], [2619, 2899, 3115], [2623, 3253, 3640], [2625, 4237, 4888], [2627, 4123, 4752], [2632, 2797, 2937], [2639, 2701, 2759], [2640, 3457, 3913], [2640, 3667, 4187], [2665, 3589, 4081], [2675, 3331, 3731], [2679, 2989, 3224], [2695, 2869, 3016], [2709, 3439, 3869], [2725, 3439, 3864], [2727, 3097, 3367], [2728, 3367, 3763], [2728, 4207, 4845], [2736, 4249, 4895], [2737, 3937, 4512], [2747, 3787, 4320], [2755, 2887, 3003], [2760, 2791, 2821], [2760, 3229, 3551], [2773, 3163, 3445], [2781, 3199, 3496], [2783, 4057, 4655], [2793, 3037, 3233], [2795, 3631, 4104], [2800, 2977, 3127], [2808, 2863, 2915], [2813, 2983, 3128], [2825, 3661, 4136], [2829, 3991, 4565], [2832, 3913, 4465], [2867, 3343, 3672], [2875, 4303, 4947], [2881, 3829, 4345], [2889, 3409, 3760], [2891, 3211, 3456], [2911, 4201, 4816], [2912, 3643, 4085], [2915, 2971, 3024], [2928, 4153, 4753], [2929, 3181, 3384], [2943, 3517, 3895], [2944, 3601, 4015], [2945, 2977, 3008], [2961, 3529, 3905], [2967, 4033, 4592], [2968, 3397, 3705], [2975, 4009, 4559], [2987, 3283, 3515], [2989, 3391, 3685], [3007, 3073, 3135], [3016, 3199, 3355], [3016, 3871, 4365], [3021, 3139, 3245], [3025, 4129, 4704], [3051, 3739, 4171], [3053, 4243, 4845], [3055, 3721, 4144], [3080, 3613, 3977], [3080, 4159, 4731], [3103, 3493, 3783], [3105, 3853, 4312], [3120, 3379, 3589], [3127, 3313, 3472], [3128, 3997, 4503], [3131, 3271, 3395], [3135, 3193, 3248], [3136, 3169, 3201], [3149, 3919, 4389], [3161, 3601, 3920], [3185, 3769, 4161], [3193, 3373, 3528], [3200, 3697, 4047], [3213, 4087, 4600], [3224, 3559, 3819], [3224, 4351, 4949], [3233, 3493, 3705], [3243, 4123, 4640], [3245, 3367, 3477], [3248, 3307, 3363], [3267, 4207, 4747], [3277, 3823, 4200], [3283, 3967, 4408], [3304, 4069, 4545], [3317, 3583, 3800], [3333, 3367, 3400], [3335, 3937, 4343], [3337, 4333, 4897], [3339, 3679, 3944], [3355, 3547, 3712], [3360, 3811, 4141], [3379, 3691, 3939], [3381, 4171, 4661], [3392, 3577, 3737], [3399, 3469, 3535], [3400, 4093, 4543], [3416, 4309, 4841], [3432, 3943, 4307], [3445, 3871, 4189], [3451, 4171, 4635], [3465, 3733, 3953], [3472, 3667, 3835], [3479, 4381, 4920], [3480, 3541, 3599], [3480, 4039, 4429], [3503, 3913, 4223], [3509, 4291, 4784], [3520, 3793, 4017], [3531, 3679, 3811], [3536, 3571, 3605], [3551, 4069, 4440], [3565, 4027, 4368], [3597, 3787, 3952], [3599, 3661, 3720], [3640, 4351, 4819], [3657, 4273, 4697], [3685, 4123, 4453], [3689, 4261, 4664], [3696, 4051, 4331], [3712, 3913, 4087], [3717, 3847, 3965], [3729, 4009, 4240], [3745, 3781, 3816], [3751, 4381, 4815], [3763, 4483, 4960], [3776, 4249, 4601], [3795, 4123, 4387], [3795, 4327, 4712], [3808, 4003, 4173], [3815, 3889, 3959], [3835, 4039, 4216], [3843, 3907, 3968], [3904, 4489, 4905], [3905, 4537, 4977], [3927, 4357, 4687], [3944, 4231, 4469], [3944, 4309, 4599], [3953, 4237, 4473], [3955, 4111, 4251], [3960, 3997, 4033], [3965, 4099, 4221], [3968, 4033, 4095], [4071, 4441, 4736], [4087, 4297, 4480], [4181, 4219, 4256], [4209, 4501, 4745], [4216, 4429, 4615], [4224, 4291, 4355], [4235, 4579, 4859], [4248, 4453, 4633], [4255, 4333, 4407], [4355, 4423, 4488], [4392, 4693, 4945], [4403, 4567, 4715], [4408, 4447, 4485], [4477, 4687, 4872], [4480, 4699, 4891], [4485, 4627, 4757], [4623, 4693, 4760], [4641, 4681, 4720], [4719, 4801, 4879], [4760, 4831, 4899], [4880, 4921, 4961]]
true