# Seeds for failure cases proptest has generated in the past. It is
# automatically read and these particular cases re-run before any
# novel cases are generated.
#
# It is recommended to check this file in to source control so that
# everyone who runs the test benefits from these saved cases.
cc 0a788d1be716731dff39490051025f728b311a7bf1437a386aace0541c6ba385 # shrinks to ops = [(true, 1796, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), (true, 1796, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0])]
cc 14822f4f04a717c8465034815780d9594e42c6b9d328e996994a0a78a7782ed5 # shrinks to ops = [(true, 1, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), (true, 128, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 56, 204, 2, 10, 33, 29, 224, 116, 71, 53, 231, 34, 220, 179, 208, 121, 26, 170, 132, 229, 96, 102, 111, 186, 83, 145, 122, 146, 180, 47, 154, 207, 126, 41, 150, 174, 251, 20, 64, 69, 193, 2, 215, 11, 43, 30, 42, 248, 126, 131, 64, 112, 255, 109, 159, 149, 102, 58, 176, 71, 78, 71, 253, 112, 55, 189, 59, 26, 154, 10, 20, 181, 236, 111, 207, 205, 218, 77, 43, 96, 236, 171, 216, 162, 221, 192, 143, 49, 97, 53, 185, 149, 244, 220, 2, 11, 180, 224, 66, 183, 61, 147, 94, 251, 94, 38, 64, 122, 80, 66, 223, 218, 142, 32, 39, 175, 0, 99, 78, 93, 78, 155, 54, 139, 60]), (true, 4047, [249, 51, 199, 39, 137, 60, 101, 49, 41, 62, 167, 99, 67, 166, 82, 115, 226, 158, 169, 141, 113, 150, 77, 17, 26, 169, 246, 63, 55, 145, 165, 120, 224, 9, 228, 241, 178, 182, 167, 224, 186, 9, 216, 100, 120, 140, 170, 59, 55, 72, 130, 188, 183, 237, 175, 106, 100, 121, 182, 255, 186, 203, 179, 174, 192, 235, 95, 110, 242]), (true, 3146, [230, 147, 233, 11, 80, 79, 5, 14, 250, 48, 1, 211, 115, 45, 164, 47, 119, 247, 236, 103, 153, 154, 132, 206, 178, 13, 51, 176, 101, 234, 175, 10, 15, 121, 31, 228, 74, 175, 205, 160, 158, 76, 9, 126, 39, 32, 70, 230, 107, 207, 148, 9, 166, 89, 76, 244, 65, 35, 167, 66, 86, 57, 150, 147, 35, 18, 212, 95, 147, 246, 189, 17, 158, 94, 105, 153, 63, 147, 86, 121, 51, 64, 182, 164, 251, 19, 12, 152, 146, 89, 155, 99, 39, 231, 11, 120, 139, 125, 42, 226, 255, 95, 183, 111, 111, 223, 218, 197, 116, 24, 75, 87, 19, 185, 83, 26, 246, 74, 230, 244, 67, 157, 218, 241, 37, 216, 187, 175, 202, 247, 26, 15, 21, 9, 31, 100, 107, 60, 26, 185, 118, 164, 122, 225, 196, 95, 215, 207, 92, 157, 180, 29, 17, 54, 199, 250, 54, 222, 48, 34, 146, 49, 38, 37, 104, 51, 59, 109, 12, 47, 13, 254, 171, 204, 63, 176, 49, 26, 74, 124, 52, 210, 217, 203, 59]), (true, 3119, [6, 222, 214, 166, 132, 93, 143, 6, 61, 32, 72, 78, 69, 223, 38, 21, 51, 6, 229, 28, 7, 46, 80, 160, 50, 74, 145, 39, 64, 213, 107, 172, 139, 116, 28, 57, 235, 198, 230, 176, 70, 86, 204, 40, 14, 142, 83, 132, 27, 238, 214, 241, 21, 99, 133, 213, 55, 187, 95, 224, 160, 123, 168, 104, 251, 118, 17, 157, 217, 179, 20, 183, 90, 194, 116, 202, 204, 159, 162, 193, 94, 224, 198, 100, 143, 152, 102, 49, 69, 196, 59, 198, 252, 228, 104, 84, 147, 43, 232, 205, 0, 173, 46, 214, 227, 185, 119, 81, 144, 26, 231, 85, 86, 165, 193, 211, 189, 127, 66, 99, 229, 175, 41, 179, 248, 18, 36, 254, 172, 105, 52, 48, 200, 137, 219, 136, 16, 198, 44, 94, 168, 92, 243, 105, 148, 28, 181, 181, 122, 53, 201, 49, 27, 84, 245]), (true, 4735, [44, 111, 103, 108, 166, 210, 134, 242, 22, 37, 252, 25, 17, 90, 82, 70, 143, 207, 188, 214, 128, 118, 128, 121, 1, 7, 74, 36, 56, 120, 222, 225, 175, 188, 119, 221, 208, 22, 159, 98, 48, 134, 147, 87, 198, 90, 220, 44, 134, 24, 132, 223, 243, 110, 86, 223, 24, 251, 32, 175, 254, 77, 176, 59, 53, 120, 234, 137, 90, 151, 245, 180, 113, 109, 197, 213, 156, 94, 214, 120, 114, 110, 89, 180, 112, 45, 73, 140, 160, 246, 6, 99, 237, 172, 85, 80, 182, 39, 183, 157, 29, 93, 201, 34, 96, 179, 27, 171, 152, 77, 113, 155]), (true, 3492, [168, 67, 242, 66, 135, 165, 237, 210, 197, 69, 1, 114, 228, 37, 218, 130, 25, 125, 171, 79, 189, 113, 22, 32, 158, 192, 101, 48, 74, 242, 98, 169, 239, 245, 8, 62, 156, 167, 139, 209, 31, 170, 16, 76, 250, 206, 21, 126, 70, 122, 76, 221, 212, 165, 108, 195, 39, 199, 229, 193, 207, 109, 141, 202, 145, 57, 68, 218, 108, 123, 92, 142, 122, 95, 164, 250, 67, 135, 42, 38, 150, 221, 79, 43, 112, 6, 224, 7, 121, 8, 4, 48, 195, 181, 102, 32, 232, 119, 203, 27, 8, 142, 92, 10, 30, 165, 49, 56, 194, 236, 156, 39, 48, 98, 54, 122, 113, 230, 19, 150, 90, 242, 0, 143, 100, 0, 162, 7, 27, 130, 28, 66, 109, 149, 13, 36, 102, 197, 241, 176, 92, 48, 212, 150, 206, 244, 118, 202, 9, 195, 209, 153, 98, 158, 77, 245, 100, 128, 21, 147, 241, 255, 73, 162, 219, 211, 57, 248, 217, 40, 236, 214, 42, 227, 31, 213, 78, 197, 214, 216]), (true, 3465, [234, 93, 68, 5, 91, 130, 147, 232, 223, 113, 60, 154, 21, 249, 234, 237, 156, 93, 159, 175, 19, 93, 110, 200, 16, 156, 138, 181, 102, 253, 232, 20, 46, 166, 92, 97, 85, 179, 252, 150, 193, 16, 54, 116, 103, 70, 49, 207, 66, 78, 30, 46, 117, 21, 168, 144, 63, 128, 146, 130, 173, 188, 33, 15, 236, 77, 12, 93, 123, 122, 33, 24, 142, 166, 169, 229, 87, 255, 122, 243, 188, 133, 12, 95, 142, 103, 70, 39, 169, 192, 80, 190, 51, 94, 87, 94, 12, 0, 57, 128, 125, 225, 231, 176, 155, 174, 92, 69, 195, 127, 149, 76, 89, 212, 116, 211, 161, 188, 28, 106, 18, 9, 68, 0, 234, 229, 53, 213, 109, 41, 59, 198, 168, 16, 48, 61, 252, 86, 173, 146, 161, 49, 173, 125, 122, 94, 10, 70, 84, 117, 124, 61, 184, 97, 145, 49, 84, 107, 98, 51, 128, 50, 208, 220, 42, 90, 196, 241, 124, 5, 51, 37, 94, 223, 174, 44, 90, 36, 136, 248, 211, 145, 71, 252, 47, 39, 138, 254, 240, 215, 40, 205, 102, 70, 187, 152, 224]), (true, 3498, [241, 163, 2, 58, 27, 108, 214, 78, 184, 71, 113, 83, 6, 248, 28, 7, 253, 237, 80, 37, 113, 65, 117, 218, 72, 19, 154, 21, 66, 186, 174, 126, 79, 1, 226, 37, 155, 36, 9, 98, 18, 31, 253, 43, 135, 187, 34, 54, 172, 125, 21, 21, 102, 191, 15, 25, 129, 63, 62, 52, 165, 5, 208, 46, 135, 23, 118, 251, 150, 15, 178, 180, 129, 161, 4, 202, 13, 148, 166, 196, 179, 252, 230, 144, 199, 248, 40, 0, 35, 219, 248, 187, 244, 18, 132, 224, 169, 96, 121, 254, 149, 255, 181, 12, 31, 54, 186, 5, 185, 122, 102, 220, 96, 96, 226, 38, 2, 205, 249, 249, 172, 182, 155, 75, 122, 234, 67, 153, 220, 153, 84, 42, 164, 132, 197, 128, 232, 54, 19, 93, 85, 233, 153, 181, 69, 110, 2, 86, 251, 198, 247, 114, 96, 57, 232, 169, 130, 146, 237, 52, 74, 104, 148, 23, 230, 213, 213, 189, 124]), (true, 3285, [114, 199, 164, 4, 135, 46, 115, 224, 227, 130, 40, 55, 124, 76, 186, 232, 120, 84, 191, 177, 126, 175, 114, 135, 85, 113, 131, 121, 251, 252, 253, 6, 188, 158, 207, 175, 144, 10, 236, 229, 31, 19, 181, 241, 159, 168, 70, 133, 14, 223, 0]), (true, 4934, [81, 131, 193, 250, 157, 6, 225, 91, 228, 110, 196, 182, 251, 248, 229, 106, 182, 96, 116, 58, 163, 138, 162, 230, 213, 238, 169, 116, 231, 19, 85, 80, 198, 152, 140, 110, 43, 41, 184, 70, 130, 153, 213, 86, 55, 37, 20, 214, 9, 240, 184, 26, 48, 231, 134, 109, 208, 58, 255, 151, 219, 139, 74, 242, 201, 107, 73, 220, 238, 184, 199, 192, 92, 60, 50, 254, 160, 244, 10, 208, 171, 35, 71, 230, 163, 151, 193, 26, 82, 97, 213, 24, 189, 67, 239, 145, 220, 60, 128, 31, 78, 151, 32, 1, 9, 142, 15, 204, 54, 27, 21, 105, 111, 5, 167, 15, 170, 133, 247, 48, 100, 157, 113, 5, 169, 12, 26, 48, 26, 233, 101, 46, 113, 54, 231, 130, 136, 116, 229, 126, 151, 141, 215, 175, 128]), (true, 4992, [216, 41, 192, 13, 67, 252, 58, 41, 188, 88, 204, 139, 193, 104, 121, 41, 36, 252, 66, 248, 249, 158, 80, 245, 156, 205, 144, 135, 31, 155, 205, 163, 29, 141, 141, 52, 37, 233, 185, 7, 208, 63, 251, 185, 196, 245, 173, 85, 202, 113, 96, 138, 233, 226, 67, 140, 144, 216, 116, 230, 141, 44, 14, 235, 71, 149, 129, 105, 116, 213, 170, 35, 62, 27, 118, 216, 80, 210, 225, 58, 135, 191, 48, 113, 187, 158, 158, 87, 20, 104, 239, 62, 202, 242, 28, 73, 240, 33, 181, 203, 227, 214, 147, 128, 118, 85, 188, 117, 69, 197, 67, 124, 180, 211, 3, 150, 181, 10, 179, 78, 91, 11, 121, 102, 37, 235, 1, 130, 41, 18, 106, 129, 117, 194, 45, 230, 225, 159, 253, 48, 127, 186, 230, 235, 12, 192, 189, 168, 30, 128, 92, 3, 33, 240, 244, 160, 182, 222, 242, 174, 86, 25, 30, 11, 212, 35, 37, 105, 47, 99, 60, 89, 249, 140, 81, 180, 239, 238, 168, 120, 153, 134, 22, 91]), (true, 4978, [49, 236, 248, 164, 58, 166, 191, 79, 183, 216, 240, 136, 193, 190, 247, 186, 41, 234, 201, 153, 72, 236, 78, 71, 248, 192, 169, 216, 92, 13, 215, 93, 182, 221, 15, 90, 100, 108, 230, 247, 222, 153, 119, 57, 62, 71, 119, 3, 143, 107, 19, 199, 62, 114, 45, 120, 48, 125, 237, 215, 224, 234, 197, 157, 79, 60, 43, 205, 128, 234, 252, 172, 85, 3, 73, 105, 149, 57, 103, 96, 149, 11, 119, 128, 37, 82, 245, 87, 196, 28, 35, 65, 209, 242, 8, 105, 243, 172, 216, 191, 176, 32, 229, 225, 248, 1, 124, 108, 99, 42, 48, 12, 198, 236, 181, 46, 109, 111, 111, 53, 215, 57]), (true, 2916, [190, 228, 26, 79, 236, 109, 20, 126, 182, 109, 189, 96, 88, 230, 23, 228, 184, 128, 191, 97, 193, 217, 73, 28, 91, 231, 210, 219, 140, 228, 35, 155, 157, 150, 237, 111, 235, 228, 45, 130, 187, 91, 208, 98, 61, 82, 129, 28, 182, 162, 202, 234, 199, 39, 187, 168, 108, 85, 51, 235, 64, 226, 26, 59, 222, 36, 132, 102, 84, 81, 85, 227, 2, 169, 251, 187, 236, 159, 65, 174, 104, 57, 146, 252, 44, 134, 0, 20, 100, 207, 117, 111]), (true, 4098, [163, 173, 174, 3, 58, 39, 81, 27, 143, 89, 60, 147, 19, 88, 23, 38, 105, 106, 153, 83, 114, 2, 165, 24, 218, 56, 128, 163, 200, 75, 246, 208, 107, 99, 123, 19, 129, 237, 21, 58, 254, 111, 139, 22, 182, 175, 218, 238, 31, 131, 191, 223, 241, 46, 94, 189, 141, 142, 159, 1, 46, 149, 141, 127, 167, 171, 186, 135, 52, 190]), (true, 4206, [112, 179, 178, 218, 9, 205, 172, 166, 84, 210, 46, 192, 231, 62, 214, 81, 162, 115, 143, 158, 69, 181, 214, 188, 134, 129, 87, 48, 112, 67, 50, 219, 213, 69, 64, 231, 119, 173, 224, 9, 228, 102, 104, 47, 15, 27, 133, 216, 4, 80, 202, 210, 50, 191, 195, 220, 5, 53, 77, 58, 125, 166, 192, 167, 140, 44, 118, 241, 66, 223, 62, 68, 148, 179, 86, 51, 142, 202, 202, 78, 248, 193, 63, 151, 103, 85, 42, 234, 124, 34, 48, 251, 90, 62, 185, 209, 66, 13, 96, 122, 179, 197, 244, 73, 3, 72, 97, 177, 220, 90, 223, 53, 144, 226, 208, 119, 124, 71, 152, 33, 243, 209, 182, 237, 72]), (true, 3338, [102, 109, 168, 21, 231, 184, 132, 167, 86, 13, 147, 73, 72, 187, 28, 162, 153, 197, 156, 130, 16, 20, 128, 167, 239, 152, 34, 226, 203, 39, 243, 203, 200, 239, 15, 187, 93, 47, 129, 180, 72, 54, 126, 140, 143, 24, 8, 63, 173, 104, 162, 236, 229, 160, 221, 121, 26, 83, 213, 61, 90, 116, 58, 59, 10, 207, 186, 11, 28, 137, 126, 136, 161, 201, 220, 64, 160, 107, 111, 114, 175, 29, 103, 225, 98, 251, 120, 197, 80, 112, 252, 118, 112, 215, 20, 57, 90, 161, 54, 137, 251, 171, 187, 209, 153, 140, 75, 114, 89, 44, 90, 66, 146, 105, 110, 200, 119, 80, 202, 107, 248, 13, 97, 141, 168, 201, 81, 136, 16, 187, 207, 168, 16, 138, 7, 62, 27, 217, 49, 26, 113, 76, 38, 195, 76, 56, 215, 108, 144, 238, 4, 60, 187, 4, 68, 16, 194, 38, 115, 62, 54, 210, 194, 139, 81, 142, 44, 39, 48, 220, 26, 84, 33, 4, 24, 89, 6, 204, 96, 236, 6, 188, 130, 77, 84, 221, 246, 236, 30, 146, 70, 78, 37, 61, 113, 143, 13, 186]), (true, 1927, [163, 241, 186, 119, 168, 101, 39, 11, 240, 168, 36, 66, 5, 186, 43, 107, 184, 190, 220, 53, 244, 103, 163, 108, 211, 153, 244, 31, 22, 223, 162, 55, 34, 227, 244, 107, 15, 209, 65, 159, 222, 213, 58, 199, 190, 223, 181, 59, 64, 250, 63, 111, 75, 209, 236, 190, 14, 177, 172, 174, 100, 172, 128, 30, 64, 7, 79, 48, 105, 240, 227, 55, 14, 91, 189, 128, 72, 248, 99, 132, 100, 247, 30, 99, 34, 183, 96, 209, 224, 92, 235, 118, 41, 33, 65, 114, 178, 2, 161, 51, 220, 130, 38, 95, 193]), (true, 1090, [95, 136, 60, 143, 237, 229, 123, 78, 74, 104, 234, 214, 254, 77, 202, 26, 59, 244, 53, 201, 190, 172, 208, 71, 18, 254, 142, 14, 110, 208, 86, 208, 183, 234, 80, 210, 228, 179, 202, 47, 115, 115, 0, 92, 134, 4, 215, 205, 218, 139, 1, 77, 242, 145, 138, 2, 253, 226, 135, 96, 144, 162, 248, 64, 104, 135, 108, 101, 191, 107, 177, 96, 241, 224, 6, 157, 106, 11, 217, 116, 178, 124, 195, 83, 220, 238, 240, 253, 232, 4, 84, 80, 240, 141, 79, 216, 195, 59, 246, 45, 32, 54, 166, 223, 42, 83, 133, 185, 191, 39, 154, 27, 29, 213, 51, 216, 160, 107, 77, 161, 192, 255, 174, 42, 7, 141, 219, 195, 232, 106, 238, 47, 48, 144, 20, 150, 27, 223, 146, 192, 242, 231, 243, 236, 98, 104, 22, 151, 225, 21, 71, 238, 220, 45, 20, 106, 227, 236, 10, 127, 33]), (true, 54, [56, 222, 173, 72, 64, 213, 175, 124, 92, 122, 119, 156, 9, 56, 194, 119, 77, 77, 245, 189, 68, 227, 4, 48, 234, 184, 92, 67, 78, 240, 71, 236, 57, 171, 22, 142, 237, 142, 188, 99, 45, 201, 42, 19, 6, 123, 99, 20, 188, 232, 55, 49, 91, 120, 169, 23, 116, 34, 12, 204, 15, 51, 136, 172, 109, 169, 65, 44, 15, 158, 19, 243, 24, 111, 92, 187, 145, 12, 57, 157, 234, 34, 83, 246, 53, 48, 202, 203, 187, 44, 41, 251, 37, 110, 122, 104, 71, 98, 80, 126, 64, 19, 12, 146, 194, 20, 73, 176]), (true, 1105, [8, 111, 182, 82, 219, 9, 232, 25, 37, 132, 45, 2, 192, 214, 139, 85, 174, 138, 243, 163, 225, 119, 84, 209, 101, 118, 213, 157, 130, 34, 226, 87, 72, 61, 119, 116, 237, 159, 153, 203, 157, 81, 147, 252, 198, 2, 72, 173, 81, 122, 186, 210, 21, 24, 55, 186, 139, 151, 177, 170, 247, 17, 189, 239, 253, 62, 75, 111, 0, 175, 71, 73, 193, 253, 202, 199, 76, 35, 184, 121, 134, 22, 4, 41, 160, 11, 1, 200, 140, 127, 10, 199, 152, 160, 252, 76, 186, 48, 252, 69, 37, 4, 24, 195, 214, 95, 47, 162, 201, 157, 196, 227, 193, 145, 168, 250, 94, 190, 138, 144, 233, 63, 100, 236, 235, 82, 151, 54, 23, 52, 9, 33, 29, 223, 254, 91, 77, 52, 235, 150, 199, 61, 126, 217, 149, 26, 240, 56, 137, 185, 41, 0, 136, 169, 207, 122, 129, 44, 241, 55, 153, 113, 28, 251, 238, 198, 167, 8, 36, 198, 0, 12, 163, 154, 149, 74, 102, 59, 47, 159, 217, 109]), (true, 574, [13, 88, 231, 200, 21, 167, 210, 101, 106, 26, 119, 193, 74, 244, 45, 38, 160, 138, 204, 189, 158, 247, 85, 144, 25, 61, 106, 57, 253, 60, 8, 179, 116, 192, 99, 101, 78, 69, 231, 133, 81, 252, 48, 218, 177, 65, 215, 241, 3, 61, 85, 21, 61, 159, 223, 137, 232, 57, 209, 63, 75, 124, 153, 8, 56, 207, 78, 159, 116, 130, 45, 123, 76, 85, 34, 45, 55, 47, 39, 5, 12, 116, 236, 18, 149, 198, 133, 35, 179, 17, 223, 151, 211, 67, 129, 180, 99, 90, 13, 44, 196, 184, 203, 22, 165, 160, 242, 54, 141, 1, 225, 128, 248, 150, 200, 58, 28, 33, 227, 137, 109, 196, 140, 199, 235, 228, 12, 38, 0, 82, 0, 190, 225, 166, 98, 135, 222, 176, 146, 3, 55, 21, 79, 4, 210, 150, 216, 120, 22, 220, 162, 228, 9, 225, 6, 189, 228, 94, 109, 123, 100, 22, 0, 61, 199, 20, 13, 83, 186, 202, 168, 72, 215, 221, 4, 214]), (true, 655, [194, 88, 59, 234, 26, 176, 36, 114, 53, 126, 3, 94, 153, 124, 133, 5, 214, 199, 35, 195, 98, 233, 30, 247, 174, 209, 148, 70, 110, 5, 112, 145, 253, 115, 87, 31, 210, 210, 45, 135, 9, 135, 5, 57, 7, 140, 148, 87, 7, 11, 8, 138, 189, 66, 255, 24, 157, 202, 254, 26, 2, 135, 128, 125, 77, 139, 134, 155, 124, 71, 223, 198, 11, 49, 90, 182, 12, 25, 250, 43, 211, 76, 97, 55, 127, 248, 135, 169, 243, 212, 203, 211, 181, 100, 25, 245, 164, 156, 8, 244, 242, 168, 63, 18, 79, 29, 86, 190, 255, 2, 40]), (true, 3224, [243, 109, 9, 192, 10, 152, 194, 35, 208, 47, 197, 116, 2, 66, 178, 193, 120, 97, 214, 164, 81, 242, 76, 197, 179, 84, 58, 51, 233, 48, 143, 249, 53, 245, 110, 208, 185, 55, 59, 195, 22, 213, 73, 247, 75, 60, 75, 171, 88, 166, 28, 199, 225, 185, 44, 202, 13, 201, 243, 81, 62, 70, 199, 148, 200, 85, 184, 164, 84, 203, 171, 216, 165, 32, 61, 249, 128, 46, 230, 195, 25, 172, 153, 172, 204, 45, 105, 16, 175, 95, 63, 183, 224, 105, 223, 190, 25, 188, 67, 167, 63, 148, 29, 54, 105, 107, 96, 156, 208, 234, 175, 126, 96, 20, 121, 230, 222, 249, 201, 187, 122, 88, 220, 98, 174, 206, 189, 37, 248, 54, 71, 72, 101, 197, 144, 125, 195, 133, 44, 228, 66, 91, 178, 2, 212, 1, 10, 6, 181, 168, 169, 190, 9, 250, 75, 177, 114, 196, 108, 233, 170]), (true, 2912, [78, 193, 139, 110, 2, 23, 163, 112, 89, 248, 248, 12, 82, 125, 4, 251, 214, 3, 224, 195, 101, 186, 84, 133, 19, 169, 153, 241, 69, 130, 209, 236, 204, 0, 170, 56, 17, 46, 148, 172, 176, 214, 104, 3, 85, 172, 227, 178, 39, 164, 128, 123, 4, 175, 211, 153, 84, 83, 247, 249, 181, 104, 226, 219, 34, 239, 73, 41, 76, 135, 4, 68, 143, 87, 83, 178, 156, 168, 234, 77, 74, 202, 191, 9, 144, 76, 98, 70, 156, 3, 243, 100, 92, 53, 29, 234, 252, 236, 133, 138, 37, 139, 41, 34, 49, 76, 84, 120, 12, 154, 158, 202, 35, 165, 204, 42, 146, 12, 139, 114, 177, 250, 4, 75, 127, 222, 169, 178, 172, 232, 205, 147, 139, 135, 7, 89, 8, 209, 52, 92, 24, 57, 155, 208, 178, 119, 209, 248, 207, 164, 225, 5, 51, 52, 249, 248, 41, 134, 62, 225, 129, 243, 103, 72, 45, 255, 111, 158, 232, 36, 97, 46, 173, 117, 27, 206, 253]), (true, 350, [127, 245, 215, 88, 244, 117, 29, 232, 82, 167, 109, 204, 128, 57, 113, 243, 219, 69, 38, 51, 11, 36, 194, 147, 196, 141, 71, 69, 169, 63, 165, 116, 192, 44, 233, 248, 178, 140, 146, 38, 221, 125, 116, 191, 166, 2, 238, 29, 81, 35, 158, 217, 73, 188, 73, 129, 231, 242, 83, 173, 235, 208, 103, 93, 186, 74, 242, 22, 44, 92, 27, 10, 118, 71, 193, 246, 105, 131, 32, 236, 120, 31, 226, 225, 133, 201, 80]), (true, 337, [253, 165, 82, 93, 194, 138, 242, 155, 105, 247, 39, 91, 214, 177, 84, 187, 243, 69, 37, 41, 208, 101, 12, 253, 137, 141, 82, 125, 107, 32, 157, 38, 9, 138, 194, 156, 1, 120, 247, 115, 84, 222, 125, 198, 23, 170, 13, 117, 24, 63, 35, 160, 149, 80, 12, 178, 239, 195, 114, 248, 64, 222, 123, 99, 169, 67, 136, 204, 189, 214, 134, 49, 107, 174, 131, 143, 179, 252, 19, 208, 40, 75, 102, 14, 77, 184, 69, 138, 218, 121, 236, 32, 66, 218, 95, 218, 160, 66, 213, 251, 106, 194, 51, 193, 194, 140, 94, 212, 120, 251, 180, 39, 255, 30, 117, 226, 97, 112, 136, 65, 169, 164, 213, 159, 37, 194, 54, 233, 182, 40, 132, 252, 9, 228, 147, 166, 247, 118, 87, 246, 64, 30, 253, 113, 51, 242, 251, 67, 252, 114, 188, 65, 82, 133, 54, 250, 180, 27, 174, 3, 160]), (true, 424, [147, 80, 252, 207, 126, 234, 42, 228, 251, 74, 233, 94, 104, 246, 149, 90, 135, 190, 63, 225, 170, 110, 38, 192, 98, 250, 170, 11, 210, 178, 27, 12, 130, 84, 30, 88, 5, 236, 127, 20, 33, 135, 13, 151, 185, 160, 225, 11, 97, 8, 204, 10, 76, 13, 32, 253, 142, 42, 251, 105, 64, 147, 210, 16, 58, 246, 88, 13, 8, 201, 51, 122, 5, 86, 237, 108, 236, 90, 237, 101, 122, 99, 231, 46, 94, 1, 58, 25, 146, 48, 177, 148, 187, 70, 242, 112, 50, 38, 233, 94, 165, 20, 132, 102, 183, 210, 169, 174, 196, 169, 91, 182, 63, 69, 231, 43, 2, 125, 171, 52, 243, 159, 3, 87, 231, 66, 251, 67, 124, 20, 241, 80, 48, 169, 79, 55, 48, 217, 59, 213, 206, 68, 149, 74, 94, 151, 199, 196, 185, 187, 115, 19, 98, 111, 94, 215, 221, 239, 118, 59, 1, 125, 190, 14, 17, 37, 219, 224, 20, 206, 184, 128, 239, 226, 226, 227, 200, 182, 183]), (true, 2903, [15, 57, 161, 229, 108, 244, 49, 206, 73, 98, 70, 139, 6, 216, 43, 158, 93, 120, 84, 225, 80, 60, 134, 216, 54, 91, 93, 225, 187, 228, 20, 0, 100, 81, 23, 193, 25, 74, 170, 244, 116, 106, 120, 135, 202, 181, 122, 234, 144, 224, 217, 189, 15, 184, 35, 103, 135, 36, 68, 30, 232, 113, 80, 44, 76, 127, 109, 51, 23, 104, 0, 71, 243, 180, 36, 227, 78, 73, 205, 133, 86, 250, 82, 241, 214, 148, 159, 115, 148, 1, 62, 10, 109, 107, 137, 208, 171, 173, 115, 167, 107, 150, 211, 54, 141, 43, 185, 147, 122, 172, 175, 214, 178, 103, 165, 19, 176, 116, 102, 127, 210, 233, 24, 82, 205, 61, 255, 52]), (true, 1565, [239, 40, 107, 52, 244, 94, 122, 154, 228, 248, 132, 36, 185, 170, 254, 92, 252, 15, 123, 234, 118, 30, 124, 209, 154, 52, 249, 216, 63, 191, 252, 112, 203, 44, 193, 213, 39, 25, 216, 68, 187, 21, 232, 252, 193, 203, 171, 159, 30, 64, 212, 245, 92, 70, 215, 49, 217, 56, 95, 16, 228, 208, 236, 21, 101, 0, 97, 135, 15, 140, 115, 30, 234, 139, 241, 114, 22, 251, 151, 203, 146, 65, 214, 122, 139, 36, 157, 248, 177, 203, 213, 19, 119, 244, 158, 118, 86, 188, 235, 203, 219, 191, 79, 92, 191, 108, 254, 236, 156, 11, 175, 78, 95, 98, 162, 116, 151, 245, 38, 129, 148, 120, 169, 244, 177, 62]), (true, 1235, [121, 99, 254, 76, 18, 47, 19, 15, 185, 116, 205, 193, 194, 81, 202, 245, 177, 159, 111, 109, 92, 23, 127, 160, 96, 26, 194, 77, 203, 255, 66, 33, 137, 107, 10, 82, 95, 51, 46, 30, 162, 36, 149, 107, 180, 225, 125, 251, 2, 149, 10, 231, 40, 178, 174, 141, 221, 73, 61, 138, 163, 45, 89, 174, 183, 74, 33, 250, 99, 106, 129, 81, 30, 81, 240, 188, 33, 193, 165, 43, 127, 113, 202, 113, 0, 56, 2, 198, 171, 216, 43, 255, 137, 94, 197, 65, 254, 53, 60, 241, 31, 103, 147, 133, 185, 28, 0, 57, 239, 137, 155, 189, 35, 165, 37, 8, 213, 174, 42, 111, 149, 66, 137, 146, 108, 163, 137, 238, 19, 59, 59, 166, 177, 148, 194, 103, 32, 87, 6, 243, 181, 197, 101]), (true, 3487, [226, 64, 215, 253, 106, 161, 29, 204, 199, 10, 15, 186, 194, 99, 42, 193, 246, 45, 152, 193, 206, 30, 129, 197, 63, 138, 194, 150, 164, 60, 114, 92, 18, 46, 179, 205, 32, 10, 175, 22, 248, 133, 139, 122, 61, 211, 80, 4, 180, 212, 149, 180, 203, 68, 55, 214, 195, 156, 73, 183, 118, 165, 22, 161, 113, 187, 191, 103, 48, 232, 254, 221, 196, 245, 74, 2, 235, 75, 39, 55, 252, 65, 31, 98, 100, 147, 27, 8, 124, 197, 68, 34, 231, 179, 30, 149, 237, 79, 13, 214]), (true, 87, [146, 215, 238, 89, 195, 23, 138, 24, 236, 82, 69, 34, 205, 107, 43, 89, 192, 169, 121, 86, 205, 53, 84, 223, 78, 34, 150, 16, 16, 26, 118, 135, 76, 160, 160, 106, 43, 168, 196, 122, 91, 146, 33, 77, 53, 63, 235, 157, 253, 115, 14, 80, 193, 214, 109, 5, 11, 219, 75, 104, 19, 0, 84, 211, 209, 39, 196, 183, 123, 116, 97, 236, 132, 15, 26, 8, 45, 134, 79, 153, 66, 70, 76, 238, 193, 164, 117, 183, 111, 75, 29, 216, 79, 191, 26, 68, 42, 7, 115, 34, 230, 201, 208, 230, 11, 100, 6, 49, 154, 251, 153, 122, 248, 18, 71, 138, 101, 109, 24, 223, 149, 135, 188, 140, 69, 105, 106, 50, 134, 44, 209, 252, 149, 12, 165, 98, 165, 101, 123, 15, 177, 91, 117, 139, 88, 212, 95, 239, 122, 111, 183, 18, 197, 113, 78, 199, 254, 52, 84, 89, 88, 142, 182, 140, 230, 101, 7, 42, 101, 167, 40, 2, 177, 248, 139, 64, 125, 254, 20, 47, 158, 115, 122, 136, 16, 211, 208, 197, 174, 111, 230, 95, 175, 24, 5, 168]), (false, 2912, []), (true, 3542, [149, 7, 246, 17, 49, 176, 245, 243, 63, 32, 38, 49, 152, 228, 228, 3, 153, 162, 166, 38, 134, 187, 253, 218, 252, 44])]
cc 18e85be3204cb945bc4ffbe62384b8cc89629ff803eddd8ad9d86a067b7e915b # shrinks to ops = [(true, 1, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), (true, 4121, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), (true, 4122, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 23, 98, 217, 244, 162, 214, 175, 41, 164, 149, 140, 7, 143, 113, 253, 255, 85, 224, 58, 106, 207, 140, 230, 156, 212, 141, 62, 223, 158, 114, 105, 217, 217, 176, 0, 146, 84, 45, 6, 38, 31, 247, 152, 111, 73, 94, 11, 57, 189, 46, 220, 205, 169, 127, 157, 62, 67, 16, 82, 92, 211, 31, 129, 191, 144, 82, 153, 197, 104, 73, 152, 101, 238, 2, 179, 105, 148, 36, 13, 240, 40, 133, 84, 220, 170, 178, 226, 40, 148, 66, 5, 41, 149, 188, 174, 162, 162, 74, 182, 43, 167, 139, 231, 131, 131, 187, 242, 76, 244, 207, 220, 104, 94, 69, 87, 23, 196, 84, 156, 161, 29, 73, 80, 140, 227, 181, 224, 211, 213, 73, 237, 91, 106, 143, 83, 153, 112, 1, 84, 106, 202]), (true, 663, [201, 229, 39, 8, 138, 146, 197, 180, 157, 76, 145, 235, 20, 102, 125, 15, 166, 133, 73, 87, 178, 94, 202, 83, 244, 4, 180, 150, 163, 3, 136, 147, 152, 62, 101, 251, 85, 64, 201, 95, 92, 27, 158, 250, 240, 185, 151, 164, 243, 220, 49, 109, 71, 80, 186, 136, 116, 232, 248, 73, 199, 234, 140, 44, 150, 149, 0, 177, 185, 225, 226, 248, 118, 82, 116, 184, 48, 16, 161, 128, 94, 156, 166, 189, 71, 207, 70, 232, 234, 36, 168, 97, 163, 54, 31, 63, 245, 176, 30, 105, 184, 55, 162, 23, 24, 118, 122, 115, 206, 96, 89, 21, 66, 93, 243, 136, 5, 85, 215, 226, 32, 174, 215, 115, 241, 190, 26, 84, 241, 145, 229, 69, 151, 153, 98, 187, 240, 114, 209, 16, 135, 208, 170, 219, 178, 215, 250, 211, 163, 37, 87, 84, 94, 67, 177, 29, 3, 97]), (true, 2064, [84, 157, 106, 168, 210, 58, 216, 181, 225, 115, 12, 77, 27, 154, 31, 126, 10, 234, 22, 239, 129, 24, 79, 156, 146, 40, 85, 172, 14, 164, 226, 175, 57, 12, 57, 157, 107, 5, 218, 167, 23, 190, 195, 210, 52, 46, 25, 94, 58, 17, 250, 211, 208, 4, 191, 150, 222, 18, 25, 202, 12, 152, 27, 147, 219, 116, 222, 181, 90, 65, 251, 232, 177, 240, 188, 121, 0, 175, 51, 131, 109, 77, 247, 239, 148, 152, 193, 250, 167, 61, 178, 43, 26, 224, 192, 98, 187, 102, 214, 182, 91, 58, 255, 134, 249, 46, 61, 253, 17, 106, 17, 111, 59, 56, 239, 137, 23, 93, 73, 58, 77, 27, 2, 191, 37, 240, 197, 26, 209]), (true, 1330, [64, 37, 180, 62, 72, 106, 110, 221, 62, 8, 226, 75, 145, 78, 249, 122, 11, 123, 64, 31, 132, 90, 17, 120, 27, 231, 95, 228, 154, 134, 8, 50, 135, 211, 152, 126, 162, 196, 39, 106, 160, 52, 222, 125, 92, 54, 107, 75, 55, 80, 96, 137, 28, 255, 6, 120, 206, 52, 218, 218, 35, 224, 171, 209, 184, 195, 227, 161, 9, 169, 36, 255, 172, 85, 114, 73, 215, 208, 57, 31, 71, 146, 100, 193, 214, 30, 218, 239, 152, 101, 7, 5, 143, 121, 38, 102, 71, 165, 231]), (true, 1026, [22, 29, 193, 169, 70, 203, 223, 242, 12, 163, 85, 187, 149, 164, 75, 15, 160, 37, 1, 198, 104, 84, 20, 147, 156, 75, 127, 30, 170, 217, 231, 63, 80, 196, 201, 178, 47, 141, 68, 173, 4, 206, 33, 37, 42, 238, 216, 103, 31, 207, 57, 132, 196, 140, 41, 113, 64, 45, 255, 229, 245, 172, 78, 244, 55, 158, 114, 138, 227, 232, 30, 124, 226, 57, 66, 38, 138, 215, 26, 189, 117, 218, 242, 111, 205, 113, 34, 102, 191, 12, 57, 188, 230, 102, 167, 132, 193, 249, 77, 97, 13, 112, 3, 116, 69, 77, 159, 246, 100, 29, 184, 245, 52, 250, 221, 9, 55, 136, 207, 172, 81, 28, 205, 54, 205, 69, 204, 49, 127, 162, 100, 101, 254, 234, 99, 166, 168, 148, 65, 169, 119, 11, 72, 82, 87, 205, 184, 218, 21, 200, 49, 222, 46, 67, 67, 26, 167, 17, 142, 135, 218, 36, 214, 115, 164, 2, 139, 54, 219, 84, 253, 248, 56, 64, 181, 51, 88, 146, 122, 209, 80, 58, 93, 215, 209, 198, 181, 177, 28, 115, 116, 129, 185, 38, 92, 195, 253]), (true, 4887, [35, 255, 108, 219, 10, 64, 44, 43, 70, 181, 104, 35, 217, 201, 139, 161, 153, 135, 75, 168, 66, 251, 240, 156, 97, 65, 188, 213, 222, 80, 111, 19, 84, 198, 23, 77, 213, 193, 29, 166, 85, 213, 245, 105, 3, 207, 162, 182, 64, 198, 32, 11, 14, 223, 134, 126, 76, 232, 113, 160, 108, 17, 32, 104, 10, 148, 175, 150, 22, 138, 60, 18, 2, 172, 42, 36, 223, 243, 108, 17, 193, 217, 196, 251, 40, 1, 229, 244, 159, 167, 82, 37, 197, 146, 189, 113, 254, 187, 116, 181, 221, 164, 132, 213, 243, 219, 193]), (true, 4120, [206, 44, 224, 8, 74, 62, 153, 81, 168, 213, 28, 32, 42, 97, 119, 38, 151, 245, 233, 53, 192, 162, 26, 139, 206, 147, 8, 244, 37, 153, 206, 155, 76, 158, 231, 191, 201, 222, 242, 74, 111, 2, 136, 48, 31, 207, 2, 17, 206, 193, 6, 189, 102, 38, 53, 220, 73, 169, 207, 126, 119, 192, 193, 68, 160, 23, 9, 200, 234, 240, 187, 108, 187, 32, 162, 61, 251, 143, 39, 100, 71, 226, 121, 34, 109, 28, 122, 8, 165, 196, 12, 24, 104, 67, 117, 133, 22, 195, 13, 26, 140, 38, 4, 64, 216, 237, 35, 82, 197, 255, 240, 37, 246, 237, 124, 160, 124, 186, 114, 218, 36, 8, 159, 220, 198, 141, 71, 109, 47, 77, 76, 63, 72, 102, 6]), (true, 1785, [127, 116, 39, 134, 7, 142, 73, 53, 183, 198, 80, 111, 214, 145, 21, 156, 105, 42, 205, 105, 42, 113, 52, 227, 135, 126, 187, 123, 212, 238, 172, 111, 167, 110, 221, 140, 186, 136, 7, 110, 119, 167, 128, 81, 54, 153, 154, 97, 184, 154, 137, 2, 227, 11, 201, 39, 25, 189, 151, 68, 170, 52, 152, 150, 80, 92, 218, 189, 9, 107, 174, 101, 175, 82, 68, 148, 128, 140, 181, 28, 12, 42, 200, 48, 176, 45, 8, 24, 31, 232, 225, 21, 117, 173, 236]), (true, 1664, [65, 172, 146, 26, 147, 82, 131, 153, 238, 0, 178, 11, 35, 136, 21, 24, 74, 235, 204, 247, 43, 140, 189, 237, 130, 168, 16, 155, 141, 7, 45, 109, 12, 131, 7, 78, 3, 26, 14, 31, 42, 147, 222, 82, 226, 138, 239, 99, 44, 180, 140, 246, 71, 236, 197, 109, 46, 227, 120, 109, 150, 119, 51, 124, 229, 84, 57, 246, 7, 150, 3, 199, 132, 72, 58, 136, 205, 60, 189, 241, 42, 41, 119, 82, 66, 181, 177, 245, 154, 144, 7, 1, 55, 64, 62, 180, 52, 98, 202, 137, 203, 185, 28, 240, 87, 112, 72, 75, 161, 128, 157, 32, 198, 231, 202, 43, 79, 251, 86, 174, 98, 105, 157, 20, 234, 45, 66, 26, 23, 243, 129, 47, 122, 8, 132, 15, 60, 108, 11, 63, 93, 71, 94, 173, 103, 226, 96, 216, 59, 162, 79, 204, 138, 104, 183, 142, 183, 148, 136, 109, 230, 197, 86, 255, 50, 175, 166, 158, 30, 240, 247, 170, 65, 180, 122, 197, 165]), (true, 2093, [225, 152, 114, 43, 125, 45, 49, 180, 197, 127, 141, 37, 147, 93, 133, 193, 179, 240, 231, 64, 109, 89, 109, 170, 201, 202, 109, 82, 84, 188, 22, 200, 220, 159, 206, 221, 192, 138, 55, 5, 91, 255, 232, 71, 79, 168, 243, 239, 204, 68, 132, 83, 127, 16, 73, 177, 129, 108, 85, 151, 232, 96, 154, 195, 49, 74, 32, 160, 9, 116, 19, 156, 174, 70, 128, 102, 155, 246, 103, 250, 199, 47, 71, 93, 62, 75, 96, 210, 182, 111, 59, 5, 190, 240, 163, 175, 22, 104, 8, 217, 197, 220, 2, 25, 243, 64, 121, 44, 253, 113, 52, 205, 178, 254, 101, 156, 250, 83, 140, 241, 130, 183, 14, 49, 28, 208, 172, 42, 224, 210, 20, 111, 57, 70, 182, 179, 22, 110, 184, 0, 136, 86, 192, 187, 175, 240, 133, 211, 69, 138, 191, 168, 56, 254, 26, 119, 225, 79, 95, 116, 229, 106, 163, 200, 223, 177, 130, 80, 54, 110, 87, 25, 29, 116, 103, 165]), (true, 926, [9, 120, 63, 94, 171, 30, 130, 184, 213, 154, 2, 116, 78, 233, 133, 201, 216, 11, 16, 190, 29, 21, 226, 30, 142, 5, 39, 251, 47, 95, 170, 210, 165, 47, 18, 255, 191, 164, 233, 81, 82, 254, 61, 175, 116, 169, 119, 50, 237, 197, 163, 65, 68, 29, 67, 124, 47, 21, 65, 116, 140, 102, 195, 203, 223, 80, 222, 252, 154, 195, 251, 16, 231, 60, 191, 21, 48, 243, 249, 169, 171, 237, 130, 78, 0, 78, 222, 161, 137]), (true, 280, [200, 13, 228, 244, 208, 23, 196, 139, 58, 34, 127, 163, 49, 226, 86, 68, 96, 40, 81, 237, 71, 17, 234, 77, 69, 200, 189, 76, 230, 231, 57, 147, 66, 185, 150, 109, 56, 138, 31, 55, 183, 83, 231, 169, 247, 106, 97, 249, 94, 178, 209, 151, 23, 48, 143, 181, 11, 139, 229, 237, 172, 90, 202, 34, 21, 115, 199, 206, 236, 180, 135, 100, 204, 66, 2, 199, 213, 44, 64, 220, 118, 100, 250, 90, 193, 227, 57, 141, 244, 191, 221, 81, 206, 135, 95, 0, 34, 168, 163, 231, 53, 208, 132, 132, 53, 41, 99, 55, 164, 47, 79, 154, 78, 1, 47, 75, 254, 84, 44, 207, 91, 179, 193, 170, 25, 159, 157, 243, 3, 155, 66, 141, 242, 135, 150, 82, 49, 248, 224, 84, 207, 167, 149, 124, 206, 220, 76, 218, 145, 218, 78, 37, 104, 38, 42, 128, 169, 90, 45, 167, 252, 60, 24, 234, 44, 105, 196, 227, 35, 210, 207, 11, 134, 225, 226, 203, 244, 189, 235, 43, 77, 147]), (true, 4284, [78, 169, 0, 27, 249, 107, 46, 23, 72, 114, 223, 65, 120, 241, 130, 97, 48, 81, 68, 82, 67, 4, 2, 88, 20, 158, 99, 58, 102, 238, 75, 255, 78, 172, 176, 24, 74, 33, 30, 165, 102, 109, 54, 27, 102, 160, 252, 127, 86, 161, 244, 19, 217, 5]), (true, 2357, [61, 58, 250, 174, 119, 27, 85, 172, 40, 153, 38, 12, 64, 184, 124, 68, 139, 87, 198, 159, 119, 179, 97, 124, 93, 253, 21, 166, 218, 7, 188, 236, 30, 216, 16, 8, 51, 83, 168, 30, 163, 89, 182, 11, 201, 40, 172, 60, 185, 157, 8, 173, 63, 184, 242, 22, 64, 12, 130, 140, 20, 168, 134, 253, 90, 182, 94, 188, 75, 201, 216, 177, 152, 31, 154, 85, 223, 43, 239, 81, 25, 247, 203, 195, 212, 62, 195, 170, 48, 33, 154, 95, 148, 91, 229, 62, 130, 190, 178, 38, 255, 248, 179, 92, 28, 226, 252, 102, 13, 50, 114, 51, 82, 144, 116, 53, 31, 129, 161, 150, 155, 14, 55, 15, 212, 22, 78, 68, 106, 217, 24, 38, 30, 33, 97, 223, 58, 235, 196, 121, 45, 112, 223, 176, 42]), (true, 2854, [217, 180, 255, 142, 104, 179, 209, 174, 85, 22, 83, 161, 52, 239, 252, 167, 154, 144, 143, 159, 66, 99, 145, 59, 26, 36, 252, 53, 224, 98, 23, 255, 249, 8, 201, 234, 208, 170, 4, 58, 115, 229, 120, 22, 162, 138, 211, 249, 150, 229, 183, 155, 222, 188, 11, 21, 132, 236, 157, 168, 160, 115, 204, 148, 124, 143, 201, 100]), (true, 2055, [3, 13, 190, 197, 126, 142, 170, 113, 182, 166, 184, 32, 37, 138, 128, 23, 199, 66, 136, 83, 156, 223, 124, 83, 215, 140, 184, 2, 144, 89, 126, 127, 244, 58, 2, 22, 88, 57, 98, 181, 142, 110, 224, 123, 29, 141, 181, 102, 162, 107, 247, 3, 216, 11, 165, 14, 208, 195, 43, 116, 191, 110, 123, 255, 218, 133, 187, 190, 135, 91, 122, 198, 202, 212, 221, 248, 173, 13, 185, 214, 96, 234, 173, 100, 138, 49, 244, 222, 47, 4, 126, 122, 207, 134, 134, 189, 241, 209, 67, 108, 12, 179, 93, 18, 216, 142, 250, 26, 19, 114, 82, 173, 159, 231, 154, 111, 79, 144, 39, 80, 38, 21, 13, 10, 20, 161, 251, 7, 165, 122, 95, 162, 27, 113, 153, 176, 220, 36, 44, 101, 124, 125, 104, 190, 247, 238, 137, 14, 86, 217, 54, 133, 154, 121, 46, 6, 18, 24, 242, 100, 17, 60]), (true, 3462, [150, 81, 188, 225, 3, 37, 4, 130, 242, 251, 149, 5, 144, 131, 168, 128, 155, 166, 37, 195, 130, 12, 9, 93, 229, 43, 239, 168, 30, 160, 49, 67, 215, 195, 103, 249, 91, 134, 232, 144, 248, 230, 86, 174, 153, 81, 175, 104, 153, 35, 75, 27, 187, 60, 218, 12, 23, 126, 139, 5, 237, 128, 185, 2, 219, 134, 182, 51, 201, 30, 224, 66, 238, 92, 181, 212, 198, 138, 27, 232, 202, 96, 249, 166, 28, 248, 164, 188, 228, 102, 169, 132, 80, 59, 13, 226, 88, 229, 48, 197, 232, 84, 65, 170, 56, 230, 56, 64, 44, 108, 48, 83, 188, 75, 26, 77, 176, 102, 168, 110, 210, 138, 57, 87, 146, 31, 72, 244, 137, 1, 21, 91, 23, 13, 1, 212, 136, 141, 214, 198, 23, 197, 142, 155, 31, 105, 87, 175, 163, 224, 30, 166, 124]), (true, 1949, [113, 21, 97, 189, 54, 28, 254, 165, 197, 19, 83, 232, 150, 33, 0, 13, 26, 128, 23, 97, 68, 96, 164, 198, 63, 227, 56, 120, 8, 39, 84, 15, 64, 219, 21, 235, 55, 208, 93, 221, 206, 171, 14, 197, 149, 43, 141, 32, 74, 193, 115, 30, 190, 204, 95, 88, 186, 50, 210, 234, 82, 254, 60, 49, 140, 127, 104, 78, 203, 229, 151, 109, 182, 175, 95, 40, 90, 179, 95, 139, 204, 177, 6, 181, 0, 29, 80, 224, 1, 222, 115, 92, 176, 185, 55, 194, 53, 108, 126, 210, 129, 1, 15, 16, 141, 163, 222, 56, 124, 113, 122, 170, 100, 92, 127, 229, 110, 7, 220, 168, 254, 224, 155, 54, 205, 227, 72, 229, 196, 242, 215, 135, 53, 91, 124, 228, 229, 29, 226, 35, 250, 250, 46, 243, 27, 203, 202, 198, 114, 115, 217, 7, 233, 238, 114, 7, 117, 115, 150, 34, 73, 241, 213, 95, 35, 173, 102, 39, 156, 220, 51, 195, 2, 43, 51, 82, 176, 218, 49, 109, 167, 32, 173, 79]), (true, 3619, [152, 195, 64, 250, 233, 201, 175, 152, 215, 230, 200, 128, 204, 106, 73, 33, 56, 110, 168, 99, 35, 239, 254, 250, 209, 163, 13, 27, 195, 173, 63, 244, 195, 2, 53, 120, 113, 78, 56, 209, 121, 233, 30, 181, 199, 157, 75, 176, 146, 173, 194, 0, 222, 32, 90, 166, 132, 151, 249, 197, 140, 214, 227, 186, 144, 150, 107, 241, 48, 158, 175, 111, 19, 107, 85, 224, 197, 135, 186, 74, 123, 217, 201, 130, 73, 133, 109, 26, 195, 158, 44, 236, 30, 170, 116, 249, 38, 39, 195, 117, 132, 103, 41, 72, 56, 10, 85, 218, 75, 2, 193, 123, 142, 142, 194, 137, 235, 179, 224, 163, 159, 14, 100, 206, 173, 86, 197, 58, 189, 142, 103, 6, 159, 39, 137, 88, 18, 253, 206, 113, 185, 106, 107, 239, 74, 165, 206, 211, 156, 27, 183, 31, 255, 191, 88, 217, 186, 72, 28, 167, 8, 193, 156, 101, 168, 161, 73, 13, 117, 113, 165]), (true, 1564, [155, 2, 195, 132, 138, 123, 110, 218, 250, 27, 111, 6, 199, 196, 14, 24, 4, 202, 210, 209, 42, 115, 71, 190, 76, 227, 55, 79, 90, 209, 223, 62, 95, 88, 26, 6, 93, 182, 213, 155, 174, 137, 64, 16, 106, 214, 183, 183, 45, 60, 211, 7, 213, 149, 97, 55, 164, 93, 105, 114, 236, 202, 62, 10, 236, 238, 255, 9, 227, 172, 99, 120, 120, 180, 166, 172, 242, 43, 52, 210, 141, 200, 57, 42, 131, 7, 250, 18, 171, 16, 116, 141, 220, 140, 240, 143, 232, 127, 236, 209, 200, 112, 243, 25, 175, 64, 50, 5, 181, 244, 90, 122, 102]), (true, 2454, [145, 180, 131, 66, 190, 23, 90, 203, 120, 251, 43, 59, 203, 107, 85, 219, 127, 200, 96, 168, 189, 196, 180, 186, 160, 147, 125, 247, 150, 128, 243, 126, 50, 93, 87, 47, 247, 195, 53, 203, 155, 142, 195, 198, 191, 110, 1, 113, 209, 0, 49, 171, 162, 84, 247, 42, 191, 58, 247, 78, 232, 70, 174, 63, 21, 86, 152, 27, 197, 41, 11, 121, 133, 255, 241, 215, 64, 196, 177, 148, 189, 211, 99, 105, 71, 113, 22, 147, 6, 190, 165, 147, 74, 39, 235, 191, 93, 76, 196, 235, 239, 217, 93, 133, 221, 199, 213, 34, 59, 202, 196, 6, 133, 85, 183, 39, 38, 39, 200, 50, 90, 214, 201, 106, 55, 117, 160, 252, 206, 105, 174, 166, 144, 1, 55, 244, 183, 113, 21, 148, 254, 89, 48, 30, 69, 104, 110, 93, 219, 152, 109, 55, 70, 135, 37, 135, 195, 111, 202, 182, 73, 171, 161, 226, 213, 197, 171, 86, 125, 15, 201, 222, 189, 10, 97, 184, 102, 136, 116, 227, 137]), (true, 3976, [100, 50, 213, 108, 114, 203, 119, 13, 106, 147, 155, 229, 239, 195, 32, 162, 91, 48, 87, 145, 170, 147, 55, 218, 197, 190, 63, 67, 130, 4, 203, 195, 104, 20, 225, 156, 6, 209, 19, 52, 178, 210, 203, 208, 235, 188, 30, 81, 159, 134, 74, 105, 127, 59, 39, 44, 117, 199, 140, 213, 153, 224, 220, 5, 10, 219, 160, 161, 76, 37, 199, 104, 14, 40, 39, 30, 84, 235, 55, 0, 22, 120, 65, 18, 136, 225, 19, 218, 213, 155, 94, 23, 100, 189, 86, 150, 26, 243, 120, 240, 86, 242, 16, 75, 41, 35, 216]), (true, 3345, [134, 200, 249, 166, 249, 18, 32, 178, 247, 58, 3, 115, 255, 253, 7, 247, 139, 95, 207, 172, 48, 251, 55, 145, 205, 57, 212, 244, 134, 1, 217, 43, 168, 37, 216, 6, 224, 166, 217, 130, 189, 201, 100, 5, 133, 181, 15, 50, 67, 115, 110, 42, 150, 182, 253, 58, 76, 80, 189, 243, 45, 27, 41, 224, 107, 85, 140, 37, 38, 2, 61, 140, 255, 10, 243, 25, 147, 204, 223, 191, 74, 57, 125, 235, 66, 181, 101, 115, 226, 171, 70, 255, 139, 178, 13, 119, 23, 119, 188, 102, 122, 158, 67, 216, 203, 239]), (true, 3982, [207, 69, 124, 122, 93, 162, 155, 14, 164, 107, 233, 154, 28, 249, 250, 72, 32, 115, 38, 86, 131, 45, 63, 34, 238, 229, 21, 109, 50, 109, 92, 228, 177, 210, 193, 107, 44, 114, 39, 28, 19, 116, 179, 174, 80, 65, 184, 63, 203, 65, 150, 114, 2, 243, 173, 27, 222, 228, 248, 224, 14, 207, 79, 75, 176, 40, 0, 182, 47, 178, 193, 143, 198, 51, 40, 226, 181, 171, 186, 220, 137, 7, 243, 20, 118, 19, 25, 226, 125, 15, 11, 202, 130, 80, 28, 39, 176, 165, 122, 241, 172, 215, 98, 212, 188, 185, 21, 136, 149, 41, 30, 60, 203, 188, 88, 90, 222, 38, 7, 17, 149, 179, 121, 116, 131, 40, 52, 83, 157, 172, 112, 216, 7, 93, 161, 172, 96, 109, 241, 39, 73, 106, 172, 65, 169, 74, 123, 105, 36, 169, 100, 17, 112, 183, 228]), (true, 1573, [225, 46, 149, 223, 251, 85, 178, 218, 173, 119, 239, 120, 120, 43, 31, 145, 195, 1, 14, 181, 172, 212, 224, 142, 176, 22, 143, 165, 79, 53, 246, 239, 157, 6, 252, 148, 113, 138, 95, 82, 111, 229, 25, 53, 216, 245, 0, 60, 193, 23, 8, 32, 95, 172]), (true, 2557, [206, 158, 90, 150, 117, 25, 176, 209, 79, 189, 71, 147, 85, 162, 3, 5, 168, 189, 161, 81, 31, 41, 174, 154, 75, 59, 236, 74, 199, 180, 107, 30, 51, 83, 64, 74, 158, 244, 116, 13, 83, 86, 154, 104, 103, 141, 251, 228, 247, 24, 64, 161, 133, 93, 238, 204, 232, 224, 67, 84, 146, 146, 72, 62, 241, 63, 245, 59, 34, 195, 189, 89, 68, 28, 129, 225, 241, 66, 20, 155, 39, 114, 195, 129, 97, 195, 146, 205, 86, 195, 108, 55, 44, 238, 52, 36, 142, 209, 125, 51, 77, 179, 38, 222, 143, 43, 135, 96, 167, 6, 104, 210, 143, 77, 250, 77, 81, 165, 19, 224, 124, 158, 234, 181, 128, 55, 7, 113, 152, 230, 199, 26, 37, 150, 101, 5, 248, 32, 23, 62, 159, 1, 252, 23, 30, 123, 235, 87, 54, 76, 247, 11, 2, 119, 230, 51, 3, 163, 59, 29, 48, 110, 50, 169, 10, 149, 120, 201, 139, 153, 132, 226]), (true, 4067, [102, 84, 87, 206, 242, 146, 40, 49, 116, 254, 209, 141, 106, 254, 242]), (true, 3184, [116, 50, 76, 112, 16, 133, 199, 169, 128, 131, 153, 55, 111, 109, 51, 126, 49, 93, 172, 76, 74, 23, 216, 55, 53, 207, 176, 18, 244, 176, 19, 22, 237, 123, 2, 52, 210, 235, 242, 121, 251, 70, 45, 136, 227, 134, 136, 114, 216, 132, 128, 6, 92, 13, 137, 145, 128, 90, 7, 123, 132, 15, 34, 21, 85, 27, 17, 64, 10, 226, 249, 237, 123, 66, 162, 220, 107, 0, 76, 50, 41, 220, 38, 63, 37, 94, 175, 149, 251, 19, 148, 175, 187, 86, 142, 6, 118, 236, 98, 255, 150, 234, 7, 223, 254, 79, 70, 220, 14, 234, 53, 3, 62, 244, 126, 96, 2, 149, 70, 144, 246, 193, 112, 142, 102, 134, 33, 91, 27, 106, 166, 87, 28, 34, 173, 34, 233, 33, 37, 124, 249, 239, 235, 10, 244, 205, 3]), (true, 2955, [156, 28, 160, 20, 150, 166, 132, 184, 242, 198, 141, 129, 186, 0, 255, 189, 68, 230, 11, 154, 70, 39, 118, 93, 51, 49, 134, 75, 140, 42, 167, 247, 85, 135, 247, 54, 150, 165, 69, 45, 57, 246, 61, 51, 170, 85, 162, 87, 58, 132, 241, 205, 223, 174, 18, 110, 84, 239, 103, 245, 199, 115, 94, 105, 232, 138, 145, 208, 116, 58, 246, 42, 117, 24, 221, 101, 139, 179, 138, 251, 186, 105, 207, 29, 113, 105, 37, 53, 93, 191, 159, 236, 42, 111, 83, 127, 65, 127, 98, 111, 10, 154, 141, 108, 125, 7, 249, 66, 79, 106, 80, 170, 49, 78, 79, 157, 95, 130, 38, 25, 168, 196, 92, 158, 223, 210, 29, 47, 33, 46, 86, 40, 244, 138, 168, 143, 82, 222, 169, 62, 33, 72, 11, 236, 228, 199, 53, 182, 2, 110, 249, 231, 92, 101, 119, 152, 131, 54, 51, 88, 4, 117, 92, 115, 189, 109, 148, 141, 200, 239, 8, 3, 105, 163, 230, 100, 194, 197, 176, 123, 229, 69, 89, 125, 53, 116]), (false, 4120, []), (true, 2034, [184, 22, 59, 177, 123, 16, 86, 11, 178, 165, 99, 212, 83, 227, 1, 183, 139, 37, 215, 18, 224, 252, 10, 67, 95, 21, 5, 155, 183, 211, 25, 37, 101, 68, 50, 165, 237]), (true, 3361, [216, 135, 247, 55, 9, 134, 22, 196, 14, 243, 211, 230, 68, 237, 167, 62, 215, 52, 222, 151, 161, 191, 254, 134, 225, 19, 66, 194, 248, 93, 109, 0, 152, 213, 90, 51, 202, 231, 94, 244, 36, 28, 214, 113, 52, 58, 123, 216, 199, 17, 122, 104, 2, 127, 204, 42]), (true, 4106, [107, 203, 123, 205, 20, 153, 28, 251, 74, 160, 48]), (true, 4678, [155, 93, 168, 89, 250, 101, 94, 44, 49, 102, 149, 89, 228, 64, 253, 225, 140, 81, 252, 84, 197, 202, 249, 84, 137, 11, 0, 64, 192, 186, 195, 66, 51, 230, 255, 105, 93, 130, 8, 82, 242, 137, 182, 191, 42, 250, 151, 188, 247, 143, 186, 191, 14, 4, 200, 6, 226, 196, 58, 175, 128, 168, 10, 230])]
