lean/SpectreKnot/Data/Level2.lean
33 lines · generated data · on GitHub ·
GENERATED by tools/gen_clusters.py from paper/code/exact/exact.py (exact arithmetic). Do not edit by hand. The level-2 supertiles at tile level, built directly from the tile placements: used only by Tests.lean.
← SpectreKnot/Data/Clusters.leanSpectreKnot.lean →
All 39 files, and the declarations of this one
1/-
2GENERATED by tools/gen_clusters.py from paper/code/exact/exact.py (exact arithmetic). Do not edit by hand.
3The level-2 supertiles at tile level, built directly from the tile placements: used only by Tests.lean.
4-/
5import SpectreKnot.Basic
7namespace SpectreKnot.Level2
9open Kind
12 | .Gamma => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (59, 6), some (59, 5), some (58, 10), some (58, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (58, 8), some (58, 7), some (58, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (24, 8), some (24, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (24, 6), some (24, 5), some (23, 10), none, none, none, none, none, some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), none, none, none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (58, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (58, 4), some (58, 3), some (57, 6), some (57, 5), some (56, 10), some (56, 9), some (16, 10), some (17, 11), some (17, 10)], [some (33, 9), some (33, 8), some (33, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (56, 8), some (56, 7), some (56, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, some (11, 5), some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (9, 8), some (9, 7), some (9, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (55, 6), some (55, 5), some (54, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), some (51, 8), some (51, 7), some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), some (51, 6), some (51, 5), some (50, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (42, 9), some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), some (42, 8), some (42, 7), none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (9, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (56, 5), some (34, 10), some (35, 11), some (35, 10)], [some (55, 9), some (55, 8), some (55, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (56, 4), some (56, 3), some (56, 2)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (50, 6), some (50, 5), none, none, none, none, none, none, some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), none, none, some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), none, none, none, none, none, none, none, none, some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), none, none, none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, none, none, none, none, none, none, some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), none, none, some (30, 6), some (30, 5), some (29, 10), some (29, 9), some (43, 10), some (44, 11), some (44, 10)], [some (50, 9), some (50, 8), some (50, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (29, 8), some (29, 7), some (29, 6)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (54, 6), some (54, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (29, 5), some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), some (29, 4), some (29, 3), some (28, 6), some (28, 5), some (27, 10), some (27, 9), some (52, 10), some (53, 11), some (53, 10)], [some (54, 9), some (54, 8), some (54, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (27, 8), some (27, 7), some (27, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (60, 5), some (60, 4), some (60, 3), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (27, 5), some (55, 4), some (55, 3), some (55, 2)], [some (61, 3), some (61, 2), some (54, 13), some (54, 12), some (54, 11), some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (56, 1), some (56, 0), some (61, 5), some (61, 4)], [some (55, 11), some (55, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (57, 4), some (57, 3), some (57, 2)], [some (61, 7), some (61, 6), some (56, 13), some (56, 12), some (56, 11), some (15, 8), some (15, 7), some (58, 2), some (58, 1), some (58, 0), some (59, 1), some (59, 0), some (61, 9), some (61, 8)], [some (57, 9), some (57, 8), some (57, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (59, 4), some (59, 3), some (59, 2)], [some (57, 11), some (57, 10), some (58, 13), some (58, 12), some (58, 11), some (6, 8), some (6, 7), none, none, none, none, some (60, 10), some (61, 11), some (61, 10)], [none, none, none, some (54, 2), some (54, 1), some (54, 0), some (61, 1), some (61, 0), some (61, 13), some (61, 12), some (59, 11), none, none, none], [some (60, 7), some (60, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (57, 1), some (57, 0), some (57, 13), some (57, 12), some (59, 13), some (59, 12), some (60, 9), some (60, 8)]]
13 | .Delta => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
14 | .Theta => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
15 | .Lambda => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
16 | .Xi => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
17 | .Pi => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
18 | .Sigma => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
19 | .Phi => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
20 | .Psi => [[some (7, 5), some (7, 4), some (7, 3), some (14, 6), some (14, 5), none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, some (68, 6), some (68, 5), some (67, 10), some (67, 9), some (7, 10), some (8, 11), some (8, 10)], [some (14, 9), some (14, 8), some (14, 7), some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), some (67, 8), some (67, 7), some (67, 6)], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)], [some (16, 5), some (16, 4), some (16, 3), some (42, 6), some (42, 5), some (41, 10), some (34, 13), some (34, 12), some (34, 11), some (33, 10), some (33, 9), some (10, 4), some (10, 3), some (10, 2)], [some (17, 3), some (17, 2), some (9, 13), some (9, 12), some (9, 11), some (33, 8), some (33, 7), some (11, 2), some (11, 1), some (11, 0), some (12, 1), some (12, 0), some (17, 5), some (17, 4)], [some (10, 9), some (10, 8), some (10, 7), some (33, 6), some (33, 5), some (32, 10), some (25, 13), some (25, 12), some (25, 11), some (24, 10), some (24, 9), some (12, 4), some (12, 3), some (12, 2)], [some (10, 11), some (10, 10), some (11, 13), some (11, 12), some (11, 11), some (24, 8), some (24, 7), none, none, none, none, some (13, 4), some (13, 3), some (13, 2)], [some (17, 7), some (17, 6), some (12, 13), some (12, 12), some (12, 11), none, none, some (14, 2), some (14, 1), some (14, 0), some (15, 1), some (15, 0), some (17, 9), some (17, 8)], [some (13, 9), some (13, 8), some (13, 7), none, none, some (0, 4), some (0, 3), some (7, 2), some (7, 1), some (7, 0), some (67, 5), some (15, 4), some (15, 3), some (15, 2)], [some (13, 11), some (13, 10), some (14, 13), some (14, 12), some (14, 11), some (67, 4), some (67, 3), some (66, 6), some (66, 5), some (65, 10), some (65, 9), some (16, 10), some (17, 11), some (17, 10)], [some (42, 9), some (42, 8), some (42, 7), some (9, 2), some (9, 1), some (9, 0), some (17, 1), some (17, 0), some (17, 13), some (17, 12), some (15, 11), some (65, 8), some (65, 7), some (65, 6)], [some (16, 7), some (16, 6), some (10, 1), some (10, 0), some (10, 13), some (10, 12), some (13, 1), some (13, 0), some (13, 13), some (13, 12), some (15, 13), some (15, 12), some (16, 9), some (16, 8)], [some (25, 5), some (25, 4), some (25, 3), some (32, 6), some (32, 5), none, none, none, none, none, none, some (19, 4), some (19, 3), some (19, 2)], [some (26, 3), some (26, 2), some (18, 13), some (18, 12), some (18, 11), none, none, some (20, 2), some (20, 1), some (20, 0), some (21, 1), some (21, 0), some (26, 5), some (26, 4)], [some (19, 9), some (19, 8), some (19, 7), none, none, none, none, none, none, none, none, some (21, 4), some (21, 3), some (21, 2)], [some (19, 11), some (19, 10), some (20, 13), some (20, 12), some (20, 11), none, none, none, none, none, none, some (22, 4), some (22, 3), some (22, 2)], [some (26, 7), some (26, 6), some (21, 13), some (21, 12), some (21, 11), none, none, some (23, 2), some (23, 1), some (23, 0), some (24, 1), some (24, 0), some (26, 9), some (26, 8)], [some (22, 9), some (22, 8), some (22, 7), none, none, none, none, none, none, none, none, some (24, 4), some (24, 3), some (24, 2)], [some (22, 11), some (22, 10), some (23, 13), some (23, 12), some (23, 11), none, none, some (12, 6), some (12, 5), some (11, 10), some (11, 9), some (25, 10), some (26, 11), some (26, 10)], [some (32, 9), some (32, 8), some (32, 7), some (18, 2), some (18, 1), some (18, 0), some (26, 1), some (26, 0), some (26, 13), some (26, 12), some (24, 11), some (11, 8), some (11, 7), some (11, 6)], [some (25, 7), some (25, 6), some (19, 1), some (19, 0), some (19, 13), some (19, 12), some (22, 1), some (22, 0), some (22, 13), some (22, 12), some (24, 13), some (24, 12), some (25, 9), some (25, 8)], [some (34, 5), some (34, 4), some (34, 3), some (41, 6), some (41, 5), none, none, none, none, none, none, some (28, 4), some (28, 3), some (28, 2)], [some (35, 3), some (35, 2), some (27, 13), some (27, 12), some (27, 11), none, none, some (29, 2), some (29, 1), some (29, 0), some (30, 1), some (30, 0), some (35, 5), some (35, 4)], [some (28, 9), some (28, 8), some (28, 7), none, none, none, none, none, none, none, none, some (30, 4), some (30, 3), some (30, 2)], [some (28, 11), some (28, 10), some (29, 13), some (29, 12), some (29, 11), none, none, none, none, none, none, some (31, 4), some (31, 3), some (31, 2)], [some (35, 7), some (35, 6), some (30, 13), some (30, 12), some (30, 11), none, none, some (32, 2), some (32, 1), some (32, 0), some (33, 1), some (33, 0), some (35, 9), some (35, 8)], [some (31, 9), some (31, 8), some (31, 7), none, none, some (18, 4), some (18, 3), some (25, 2), some (25, 1), some (25, 0), some (11, 5), some (33, 4), some (33, 3), some (33, 2)], [some (31, 11), some (31, 10), some (32, 13), some (32, 12), some (32, 11), some (11, 4), some (11, 3), some (10, 6), some (10, 5), some (9, 10), some (9, 9), some (34, 10), some (35, 11), some (35, 10)], [some (41, 9), some (41, 8), some (41, 7), some (27, 2), some (27, 1), some (27, 0), some (35, 1), some (35, 0), some (35, 13), some (35, 12), some (33, 11), some (9, 8), some (9, 7), some (9, 6)], [some (34, 7), some (34, 6), some (28, 1), some (28, 0), some (28, 13), some (28, 12), some (31, 1), some (31, 0), some (31, 13), some (31, 12), some (33, 13), some (33, 12), some (34, 9), some (34, 8)], [some (43, 5), some (43, 4), some (43, 3), some (64, 6), some (64, 5), some (63, 10), some (61, 13), some (61, 12), some (61, 11), some (60, 10), some (60, 9), some (37, 4), some (37, 3), some (37, 2)], [some (44, 3), some (44, 2), some (36, 13), some (36, 12), some (36, 11), some (60, 8), some (60, 7), some (38, 2), some (38, 1), some (38, 0), some (39, 1), some (39, 0), some (44, 5), some (44, 4)], [some (37, 9), some (37, 8), some (37, 7), some (60, 6), some (60, 5), some (59, 10), some (52, 13), some (52, 12), some (52, 11), some (51, 10), some (51, 9), some (39, 4), some (39, 3), some (39, 2)], [some (37, 11), some (37, 10), some (38, 13), some (38, 12), some (38, 11), some (51, 8), some (51, 7), none, none, none, none, some (40, 4), some (40, 3), some (40, 2)], [some (44, 7), some (44, 6), some (39, 13), some (39, 12), some (39, 11), none, none, some (41, 2), some (41, 1), some (41, 0), some (42, 1), some (42, 0), some (44, 9), some (44, 8)], [some (40, 9), some (40, 8), some (40, 7), none, none, some (27, 4), some (27, 3), some (34, 2), some (34, 1), some (34, 0), some (9, 5), some (42, 4), some (42, 3), some (42, 2)], [some (40, 11), some (40, 10), some (41, 13), some (41, 12), some (41, 11), some (9, 4), some (9, 3), some (16, 2), some (16, 1), some (16, 0), some (65, 5), some (43, 10), some (44, 11), some (44, 10)], [some (64, 9), some (64, 8), some (64, 7), some (36, 2), some (36, 1), some (36, 0), some (44, 1), some (44, 0), some (44, 13), some (44, 12), some (42, 11), some (65, 4), some (65, 3), some (65, 2)], [some (43, 7), some (43, 6), some (37, 1), some (37, 0), some (37, 13), some (37, 12), some (40, 1), some (40, 0), some (40, 13), some (40, 12), some (42, 13), some (42, 12), some (43, 9), some (43, 8)], [some (52, 5), some (52, 4), some (52, 3), some (59, 6), some (59, 5), none, none, none, none, none, none, some (46, 4), some (46, 3), some (46, 2)], [some (53, 3), some (53, 2), some (45, 13), some (45, 12), some (45, 11), none, none, some (47, 2), some (47, 1), some (47, 0), some (48, 1), some (48, 0), some (53, 5), some (53, 4)], [some (46, 9), some (46, 8), some (46, 7), none, none, none, none, none, none, none, none, some (48, 4), some (48, 3), some (48, 2)], [some (46, 11), some (46, 10), some (47, 13), some (47, 12), some (47, 11), none, none, none, none, none, none, some (49, 4), some (49, 3), some (49, 2)], [some (53, 7), some (53, 6), some (48, 13), some (48, 12), some (48, 11), none, none, some (50, 2), some (50, 1), some (50, 0), some (51, 1), some (51, 0), some (53, 9), some (53, 8)], [some (49, 9), some (49, 8), some (49, 7), none, none, none, none, none, none, none, none, some (51, 4), some (51, 3), some (51, 2)], [some (49, 11), some (49, 10), some (50, 13), some (50, 12), some (50, 11), none, none, some (39, 6), some (39, 5), some (38, 10), some (38, 9), some (52, 10), some (53, 11), some (53, 10)], [some (59, 9), some (59, 8), some (59, 7), some (45, 2), some (45, 1), some (45, 0), some (53, 1), some (53, 0), some (53, 13), some (53, 12), some (51, 11), some (38, 8), some (38, 7), some (38, 6)], [some (52, 7), some (52, 6), some (46, 1), some (46, 0), some (46, 13), some (46, 12), some (49, 1), some (49, 0), some (49, 13), some (49, 12), some (51, 13), some (51, 12), some (52, 9), some (52, 8)], [some (61, 5), some (61, 4), some (61, 3), some (63, 6), some (63, 5), none, none, none, none, none, none, some (55, 4), some (55, 3), some (55, 2)], [some (62, 3), some (62, 2), some (54, 13), some (54, 12), some (54, 11), none, none, some (56, 2), some (56, 1), some (56, 0), some (57, 1), some (57, 0), some (62, 5), some (62, 4)], [some (55, 9), some (55, 8), some (55, 7), none, none, none, none, none, none, none, none, some (57, 4), some (57, 3), some (57, 2)], [some (55, 11), some (55, 10), some (56, 13), some (56, 12), some (56, 11), none, none, none, none, none, none, some (58, 4), some (58, 3), some (58, 2)], [some (62, 7), some (62, 6), some (57, 13), some (57, 12), some (57, 11), none, none, some (59, 2), some (59, 1), some (59, 0), some (60, 1), some (60, 0), some (62, 9), some (62, 8)], [some (58, 9), some (58, 8), some (58, 7), none, none, some (45, 4), some (45, 3), some (52, 2), some (52, 1), some (52, 0), some (38, 5), some (60, 4), some (60, 3), some (60, 2)], [some (58, 11), some (58, 10), some (59, 13), some (59, 12), some (59, 11), some (38, 4), some (38, 3), some (37, 6), some (37, 5), some (36, 10), some (36, 9), some (61, 10), some (62, 11), some (62, 10)], [some (63, 9), some (63, 8), some (63, 7), some (54, 2), some (54, 1), some (54, 0), some (62, 1), some (62, 0), some (62, 13), some (62, 12), some (60, 11), some (36, 8), some (36, 7), some (36, 6)], [some (61, 7), some (61, 6), some (55, 1), some (55, 0), some (55, 13), some (55, 12), some (58, 1), some (58, 0), some (58, 13), some (58, 12), some (60, 13), some (60, 12), some (61, 9), some (61, 8)], [some (69, 5), some (69, 4), some (69, 3), none, none, some (54, 4), some (54, 3), some (61, 2), some (61, 1), some (61, 0), some (36, 5), some (64, 4), some (64, 3), some (64, 2)], [some (70, 3), some (70, 2), some (63, 13), some (63, 12), some (63, 11), some (36, 4), some (36, 3), some (43, 2), some (43, 1), some (43, 0), some (65, 1), some (65, 0), some (70, 5), some (70, 4)], [some (64, 11), some (64, 10), some (43, 13), some (43, 12), some (43, 11), some (42, 10), some (16, 13), some (16, 12), some (16, 11), some (15, 10), some (15, 9), some (66, 4), some (66, 3), some (66, 2)], [some (70, 7), some (70, 6), some (65, 13), some (65, 12), some (65, 11), some (15, 8), some (15, 7), some (67, 2), some (67, 1), some (67, 0), some (68, 1), some (68, 0), some (70, 9), some (70, 8)], [some (66, 9), some (66, 8), some (66, 7), some (15, 6), some (15, 5), some (14, 10), some (7, 13), some (7, 12), some (7, 11), some (6, 10), some (6, 9), some (68, 4), some (68, 3), some (68, 2)], [some (66, 11), some (66, 10), some (67, 13), some (67, 12), some (67, 11), some (6, 8), some (6, 7), none, none, none, none, some (69, 10), some (70, 11), some (70, 10)], [none, none, none, some (63, 2), some (63, 1), some (63, 0), some (70, 1), some (70, 0), some (70, 13), some (70, 12), some (68, 11), none, none, none], [some (69, 7), some (69, 6), some (64, 1), some (64, 0), some (64, 13), some (64, 12), some (66, 1), some (66, 0), some (66, 13), some (66, 12), some (68, 13), some (68, 12), some (69, 9), some (69, 8)]]
23 | .Gamma => [0, 23, 46, 88, 130, 145, 160]
24 | .Delta => [0, 42, 57, 91, 114, 156, 182]
25 | .Theta => [0, 42, 57, 110, 125, 167, 182]
26 | .Lambda => [0, 42, 57, 91, 114, 167, 182]
27 | .Xi => [0, 23, 57, 110, 125, 167, 182]
28 | .Pi => [0, 23, 57, 91, 114, 167, 182]
29 | .Sigma => [0, 26, 41, 75, 98, 140, 182]
30 | .Phi => [0, 42, 57, 91, 125, 167, 182]
31 | .Psi => [0, 23, 57, 91, 125, 167, 182]
33end SpectreKnot.Level2