# 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 e736dc148a9198a37778f9af9bbe471e380b4291fda588425af39eb845dcd125 # shrinks to optimize = false, a = {0, 2, 1}, b = {5, 3, 4}
cc 3577d7c1bed81eb540378eb9302faae32b2c0d999a2258cdc9672ddc2a975a0d # shrinks to optimize = false, a = {1, 0, 2}, b = {5, 4, 3}
cc d43dba32b6455047e6da096957459c36d2f6e286d3d80281c11f7e5cd171ccd4 # shrinks to optimize = false, a = {2, 0, 1}, b = {16331, 11707, 4441, 6615, 14646, 3391, 6951, 14333, 502, 12756, 7730, 6877, 12745, 5952, 3114, 9555, 10623, 14863, 13170, 10156, 1475, 29, 12674, 16093, 8125, 16318, 14798, 14827, 3073, 12897, 3751, 10754, 9285, 1937, 10416, 13194, 11415, 10514, 3488, 11260, 13580, 4118, 15420, 2780, 12772, 5916, 5844, 7787, 2593, 4301, 1844, 6952, 1013, 3489, 14053, 11872, 1863, 12257, 1758, 10629, 5912, 12677, 13421, 7483, 9300, 15594, 13234, 621, 6431, 6979, 856, 2868, 10282, 2733, 14444, 9386, 5928, 5377, 5668, 2824, 9497, 12212, 520, 1424, 12389, 3426, 6467, 9521, 1772, 3903, 12609, 12000, 9897, 10512, 14953, 16325, 8881, 12353, 11938, 8425, 4147, 3239, 2803, 16381, 13981, 10866, 9210, 6350, 1617, 2368, 14327, 1754, 12076, 12928, 9164, 3425, 2426, 8045, 9735, 10991, 9061, 1205, 3836, 4816, 2259, 14696, 13300, 2455, 12679, 107, 1702, 6925, 1829, 6587, 10266, 3034, 14837, 15826, 2902, 10206, 8942, 5867, 8077, 16240, 3020, 10428, 13168, 12112, 15433, 10672, 11867, 15559, 16171, 7113, 387, 1095, 13334, 11973, 14552, 14793, 1806, 14198, 12045, 4134, 10610, 8148, 8705, 6024, 9873, 15765, 472, 11901, 3656, 15574, 1653, 7749, 16048, 5101, 13852, 6293, 7906, 15237, 15371, 10024, 13485, 4680, 2530, 7957, 15042, 13219, 7726, 9695, 3227, 11536, 6424, 11425, 16305, 9548, 6802, 12661, 10539, 7887, 14921, 12402, 3928, 5817, 7426, 15914, 3503, 13204, 6755, 2515, 11303, 2287, 3472, 8591, 11868, 13080, 588, 5710, 11600, 13959, 1532, 8759, 14805, 15873, 11951, 2810, 4883, 11639, 9839, 14258, 12647, 3128, 1138, 7516, 13985, 4539, 8962, 12825, 15593, 2168, 6774, 2658, 15764, 9898, 3741, 12072, 10558, 2355, 5857, 1422, 54, 12052, 16099, 1708, 4059, 4763, 7316, 9315, 13970, 11831, 2807, 1338, 11439, 4736, 2045, 6275, 6302, 1676, 8325, 2473, 283, 12845, 7380, 1514, 8264, 13029, 10237, 10598, 11884, 2493, 7532, 9998, 6581, 14284, 8590, 7741, 10101, 5593, 3373, 12554, 743, 1495, 10209, 6203, 10401, 13215, 6585, 10951, 15105, 2534, 7941, 1554, 1950, 10656, 2386, 6654, 7624, 13417, 8129, 5709, 15723, 3990, 3401, 9129, 9057, 11207, 14400, 1037, 14005, 11198, 12291, 13709, 11093, 4679, 15552, 3597, 7109, 10864, 1794, 3528, 12559, 15573, 12268, 5412, 4571, 6773, 7268, 556, 3834, 5641, 15167, 10683, 4145, 12804, 8342, 5786, 7798, 4756, 10940, 16369, 1724, 13552, 55, 15637, 6781, 6422, 223, 2997, 8246, 16197, 10217, 4670, 4333, 10581, 10435, 7088, 15598, 2969, 8644, 101, 2815, 2521, 6567, 12867, 16100, 9668, 11334, 11068, 90, 9689, 4170, 3103, 13392, 2169, 14260, 3691, 2844, 8386, 1408, 13973, 4395, 7155, 5893, 13700, 9180, 1703, 3884, 11213, 1427, 7782, 10932, 5552, 13590, 5267, 12346, 317, 4405, 10257, 250, 11856, 12960, 5656, 7713, 7284, 8553, 5077, 15262, 13351, 10087, 15355, 12468, 7837, 10124, 14283, 14238, 12555, 15580, 4653, 269, 13937, 11422, 7880, 6210, 188, 12865, 11386, 9023, 7065, 11154, 3848, 8172, 698, 11055, 11970, 11760, 3891, 1256, 4362, 7466, 2933, 409, 11191, 11113, 13865, 8662, 4957, 4655, 7150, 392, 2354, 11005, 10719, 14101, 3364, 14240, 4683, 8556, 3966, 12392, 259, 194, 12915, 13054, 10847, 6154, 6249, 5449, 1707, 10933, 6988, 15716, 1351, 7731, 12209, 14547, 14141, 10759, 5427, 10477, 8485, 15296, 2280, 312, 2173, 13826, 4054, 14316, 862, 6760, 6191, 1529, 2095, 9574, 10363, 7616, 15773, 4751, 3340, 13651, 10636, 10986, 12622, 12856, 4911, 746, 5155, 10682, 11230, 9222, 1004, 14665, 5922, 14556, 12734, 8880, 8859, 6725, 1170, 15425, 8007, 9661, 6684, 15203, 1272, 5693, 14349, 170, 9891, 1868, 11655, 8490, 4460, 11763, 12287, 4529, 6477, 2910, 13026, 6073, 7944, 3251, 13093, 3154, 16327, 13030, 1925, 8388, 693, 6030, 4899, 13096, 7629, 11966, 4649, 10612, 9939, 375, 12779, 11248, 9171, 4925, 14429, 7588, 1606, 7645, 7986, 13383, 4257, 11897, 13266, 8916, 9161, 3753, 720, 13446, 3327, 3807, 1620, 2417, 12235, 11737, 14576, 15460, 2036, 2524, 466, 1364, 1526, 6666, 3115, 7172, 12125, 8789, 4481, 480, 4684, 13748, 949, 10678, 11428, 10246, 5452, 9368, 10762, 6919, 5996, 4191, 7994, 1454, 6254, 1116, 14195, 6406, 3386, 6634, 419, 11212, 12542, 9551, 629, 1645, 8577, 9257, 3186, 13241, 157, 3606, 1344, 6689, 8856, 10250, 15547, 5109, 339, 4677, 10413, 2636, 7670, 15762, 1065, 6170, 10552, 13084, 5510, 8245, 7220, 5169, 4413, 3083, 15941, 14625, 5094, 3513, 7200, 3762, 3534, 9635, 9131, 5975, 9119, 5312, 1565, 5429, 11164, 7373, 5685, 747, 3666, 3061, 8093, 16295, 2353, 831, 13738, 8413, 5479, 10335, 4473, 653, 3259, 840, 79, 11620, 13745, 7334, 10230, 4662, 8900, 16302, 14411, 13577, 2099, 13418, 13758, 4734, 15003, 11147, 5785, 301, 14077, 3252, 5389, 159, 7694, 11106, 11614, 12217, 13473, 8351, 2657, 15139, 7209, 11855, 1597, 7548, 15002, 12680, 9106, 4074, 10690, 6638, 14743, 1959, 6778, 9428, 6407, 835, 1076, 1129, 3250, 818, 9157, 7748, 15566, 9491, 11882, 5458, 16009, 5519, 6001, 13500, 1931, 12194, 9074, 2555, 8322, 3932, 15528, 7060, 8335, 4097, 3761, 12027, 14448, 6262, 9595, 8972, 10959, 937, 12977, 10531, 7480, 12279, 271, 5287, 1099, 15072, 6655, 10788, 4805, 1502, 11783, 15851, 14778, 5249, 10453, 10529, 10443, 35, 4177, 6218, 8028, 8109, 5233, 6323, 12585, 6332, 11160, 897, 783, 7703, 3845, 4793, 9630, 3561, 4112, 12993, 4084, 153, 8186, 4532, 173, 9822, 9358, 7418, 1835}
cc 474775d8eee5ed37645481d6eb1062a2de35b70e9e0760ee24d157d8c0fe7923 # shrinks to optimize = false, a = {11069, 9025, 8564, 6398, 7017, 2257, 8175, 10287, 8474, 10009, 8134, 5719, 13784, 10521, 6526, 2417, 146, 7, 5, 4346, 15862, 10080, 147, 16217, 1939, 1219, 16008, 68, 12656, 12102, 14254, 15004, 13825, 13151, 9, 27, 7304, 8216, 964, 14126, 3278, 8305, 8174, 3568, 12459, 14397, 14, 15797, 13489, 15320, 4750, 6084, 1265, 2410, 14875, 705, 783, 5096, 3840, 15491, 7612, 8716, 6586, 280, 2331, 14486, 6263, 15980, 11991, 15, 15165, 10176, 5977, 8166, 10752, 1798, 9870, 13627, 10449, 9412, 3010, 10295, 6434, 5618, 13413, 6668, 7130, 13924, 247, 1596, 8522, 2947, 3146, 11, 16013, 8611, 1516, 13942, 14183, 1528, 12116, 5118, 1109, 12334, 13289, 14575, 1314, 3333, 10027, 13009, 15164, 698, 10431, 6149, 9302, 7184, 6784, 2, 15038, 10147, 13674, 8896, 6682, 13052, 10254, 12, 2577, 10894, 4921, 14713, 15500, 14883, 5395, 4204, 7741, 634, 13390, 12658, 6874, 906, 10410, 14781, 14256, 5908, 1464, 2537, 11440, 14146, 16200, 11345, 4955, 14208, 2576, 314, 15977, 1775, 11541, 13343, 15841, 3, 9696, 16053, 14152, 7456, 9996, 7694, 986, 9327, 16244, 6791, 11045, 7932, 1800, 12508, 4722, 5357, 6961, 5215, 6534, 1981, 2656, 10442, 12428, 5642, 12154, 4449, 9679, 10847, 12633, 9433, 12356, 5240, 10954, 11109, 4, 14583, 16, 2382, 13595, 363, 3246, 4710, 7268, 6228, 2933, 14966, 4450, 6965, 5057, 7520, 11860, 26, 6301, 9354, 8693, 7771, 5913, 768, 8821, 13532, 6920, 7012, 13551, 11218, 11178, 5325, 16318, 8600, 7271, 1869, 2499, 14009, 9878, 1176, 13568, 13, 6980, 4587, 997, 15738, 8487, 2178, 15252, 6115, 8, 2398, 1399, 17, 9221, 15318, 13021, 12710, 1527, 3061, 8254, 2833, 5260, 1, 2464, 12329, 4148, 5733, 15285, 2154, 6002, 16141, 6365, 1022, 11878, 11154, 8689, 3268, 0, 15382, 6597, 13622, 14706, 10854, 6486, 328, 3157, 148, 15679, 10537, 14550, 10269, 6189, 14049, 8864, 7531, 1962, 3726, 1236, 9045, 8470, 11479, 883, 11629, 3233, 3138, 9662, 3690, 8306, 2215, 685, 12062, 10, 13272, 5310, 13450, 1904, 12793, 11909, 5009, 15324, 14064, 13438, 9039, 5723, 10167, 4474, 12975, 4118, 3695, 1220, 14993, 9948, 4884, 8295, 6497, 9256, 11262, 12956, 12885, 7015, 972, 1804, 9447, 11888, 11122, 9668, 895, 12602, 6, 7764, 11586, 4022, 10718, 1141, 10372, 82, 8695, 6066, 11892, 3096, 12320, 9848, 13032, 10849, 9712, 8177, 10447, 7522, 11539, 4168, 4674, 11530, 5805}, b = {15962, 14095, 11552, 5575, 12765, 6674, 13568, 12749, 7368, 2519, 5, 7581, 9229, 8779, 8285, 16112, 9217, 7579, 15249, 8143, 7617, 8138, 14425, 14384, 4577, 2106, 9828, 12635, 11745, 3674, 12227, 1263, 4061, 6930, 7729, 12283, 8281, 232, 14200, 2726, 4060, 9095, 11359, 12641, 3088, 11957, 2543, 8938, 418, 1459, 6694, 13680, 2151, 13113, 10910, 8484, 991, 3381, 14185, 13170, 12198, 13205, 3432, 1967, 12978, 15201, 5436, 3709, 15017, 8201, 10626, 11445, 16283, 7981, 10537, 11703, 9047, 15125, 9712, 15796, 9212, 8859, 9152, 15561, 4713, 16016, 8132, 4139, 12360, 14917, 13890, 12684, 12258, 12203, 13321, 1397, 10479, 8257, 817, 4941, 5046, 12905, 8983, 13984, 15217, 14837, 15218, 2534, 624, 9506, 9192, 5536, 15780, 5148, 11230, 12087, 12074, 13008, 562, 6525, 10323, 14069, 12568, 620, 10613, 12631, 13124, 15828, 5564, 12828, 15281, 4602, 8695, 1139, 5872, 6668, 15351, 10142, 11387, 12506, 690, 10371, 4850, 3913, 11041, 13328, 5909, 13516, 7320, 11803, 13721, 6199, 3268, 3419, 4667, 7564, 644, 15673, 14206, 16227, 542, 13693, 7242, 12186, 598, 4048, 4225, 2743, 9468, 3124, 2779, 1225, 10282, 16320, 9132, 10986, 4187, 5707, 6204, 16092, 11731, 773, 5586, 1360, 340, 13563, 10014, 3105, 11431, 15490, 1775, 11751, 13465, 1267, 13531, 1443, 5800, 5532, 1769, 7677, 15469, 10169, 4638, 10243, 6655, 1413, 13479, 11780, 10264, 4175, 13941, 10979, 12895, 5238, 13873, 3331, 13852, 7033, 15791, 7337, 9431, 4449, 3975, 9706, 14094, 520, 8188, 14475, 1280, 9289, 10847, 9196, 8297, 5923, 7400, 4238, 2754, 11926, 9333, 14138, 1752, 6714, 565, 8430, 12784, 6625, 6394, 3163, 2774, 8782, 13304, 4361, 4321, 9693, 13265, 15956, 1472, 9173, 2970, 6876, 3705, 3304, 3325, 5426, 1686, 7901, 4057, 158, 3755, 7152, 2460, 11122, 5222, 11153, 9538, 2368, 10224, 6571, 7326, 1269, 7360, 12371, 8776, 8507, 14367, 7871, 10729, 9761, 5068, 9561, 492, 8437, 8346, 11876, 6916, 4607, 14937, 8253, 14121, 13357, 1255, 430, 6465, 3369, 4588, 10218, 3346, 6964, 11562, 3617, 14549, 1777, 1418, 1356, 4733, 185, 7837, 12419, 16302, 14899, 16327, 12977, 9042, 5780, 8757, 12595, 4343, 14019, 3991, 8627, 10459, 15715, 12637, 2401, 4028, 7354, 10558, 13534, 2905, 12412, 1331, 14059, 8527, 6993, 5203, 15659, 13302, 9352, 8309, 8046, 6177, 6086, 1620, 6702, 15388, 5412, 3545, 16151, 9328, 14497, 619, 13659, 5998, 1346, 8995, 9258, 16167, 12965, 8700, 7589, 13334, 9227, 12487, 12480, 14551, 1438, 4842, 15806, 9799, 10768, 4783, 3688, 4390, 9567, 8419, 13785, 10381, 15722, 14906, 3714, 2019, 15798, 6855, 10713}
