Theory Result_File_Coarse

theory Result_File_Coarse
imports
  "HOL-ODE-Numerics.ODE_Numerics"
  Result_Elements
begin

definition "coarse_results = [
  Result False (ldec (46.5000000000)) (udec (53.7000000000)) (ldec (0.3027220600)) (ldec (7500.0000000000)) (-1129) (-1125) (-239) (-223) (-1267) (-727) (-1257) (-725),
  Result False (ldec (46.4000000000)) (udec (53.6000000000)) (ldec (0.3065558800)) (ldec (7000.0000000000)) (-1123) (-1119) (-239) (-217) (-1265) (-727) (-1253) (-725),
  Result False (ldec (46.3956200000)) (udec (53.3477100000)) (ldec (0.3103469500)) (ldec (6500.0000000000)) (-1117) (-1113) (-239) (-211) (-1261) (-727) (-1247) (-725),
  Result False (ldec (46.2369100000)) (udec (53.1923800000)) (ldec (0.3122256700)) (ldec (6000.0000000000)) (-1111) (-1107) (-237) (-205) (-1257) (-727) (-1241) (-725),
  Result False (ldec (46.0436500000)) (udec (52.9541800000)) (ldec (0.3150818450)) (ldec (5500.0000000000)) (-1105) (-1101) (-235) (-199) (-1253) (-725) (-1237) (-723),
  Result False (ldec (45.9594200000)) (udec (52.6974700000)) (ldec (0.3210552550)) (ldec (5000.0000000000)) (-1099) (-1095) (-229) (-193) (-1251) (-727) (-1231) (-723),
  Result False (ldec (45.7454400000)) (udec (52.3441000000)) (ldec (0.3256527800)) (ldec (4500.0000000000)) (-1093) (-1089) (-223) (-185) (-1247) (-725) (-1229) (-723),
  Result False (ldec (45.2772800000)) (udec (51.4404300000)) (ldec (0.3400063300)) (ldec (4000.0000000000)) (-1087) (-1083) (-209) (-177) (-1245) (-725) (-1225) (-723),
  Result False (ldec (45.0490200000)) (udec (51.1730800000)) (ldec (0.3454558150)) (ldec (3500.0000000000)) (-1081) (-1077) (-203) (-171) (-1241) (-725) (-1221) (-721),
  Result False (ldec (44.9022700000)) (udec (50.9646600000)) (ldec (0.3477751450)) (ldec (3000.0000000000)) (-1075) (-1071) (-197) (-163) (-1237) (-725) (-1217) (-721),
  Result False (ldec (44.5486800000)) (udec (50.8152000000)) (ldec (0.3503280800)) (ldec (2500.0000000000)) (-1069) (-1065) (-191) (-157) (-1233) (-725) (-1213) (-721),
  Result False (ldec (44.3725200000)) (udec (50.6814500000)) (ldec (0.3526535850)) (ldec (2000.0000000000)) (-1063) (-1059) (-183) (-151) (-1229) (-723) (-1209) (-721),
  Result False (ldec (43.8671300000)) (udec (50.4821000000)) (ldec (0.3557136300)) (ldec (1500.0000000000)) (-1057) (-1053) (-177) (-145) (-1225) (-723) (-1205) (-721),
  Result False (ldec (43.7101600000)) (udec (50.2445900000)) (ldec (0.3586805750)) (ldec (926.2153250000)) (-1051) (-1047) (-173) (-137) (-1221) (-723) (-1201) (-719),
  Result False (ldec (43.7017800000)) (udec (49.9682000000)) (ldec (0.3641661600)) (ldec (921.4578200000)) (-1045) (-1041) (-165) (-131) (-1217) (-723) (-1197) (-719),
  Result False (ldec (43.6131200000)) (udec (49.6671700000)) (ldec (0.3707230600)) (ldec (901.7779050000)) (-1039) (-1035) (-159) (-127) (-1213) (-723) (-1193) (-719),
  Result False (ldec (43.2713700000)) (udec (49.4741300000)) (ldec (0.3716883550)) (ldec (898.1764550000)) (-1033) (-1029) (-155) (-119) (-1209) (-721) (-1189) (-719),
  Result False (ldec (43.1388600000)) (udec (49.0807200000)) (ldec (0.3792881650)) (ldec (893.4427950000)) (-1027) (-1023) (-147) (-113) (-1205) (-721) (-1183) (-717),
  Result False (ldec (42.8636900000)) (udec (48.9660000000)) (ldec (0.3726286650)) (ldec (889.1682700000)) (-1021) (-1017) (-141) (-107) (-1201) (-721) (-1179) (-717),
  Result False (ldec (42.5614900000)) (udec (48.6032100000)) (ldec (0.3787793450)) (ldec (884.6071300000)) (-1015) (-1011) (-133) (-101) (-1197) (-721) (-1175) (-717),
  Result False (ldec (42.4905400000)) (udec (48.3510500000)) (ldec (0.3829219150)) (ldec (880.1381400000)) (-1009) (-1005) (-127) (-95) (-1193) (-721) (-1171) (-717),
  Result False (ldec (42.2516300000)) (udec (48.0481400000)) (ldec (0.3879614750)) (ldec (860.6210550000)) (-1003) (-999) (-123) (-89) (-1189) (-719) (-1167) (-717),
  Result False (ldec (42.0492800000)) (udec (47.7468100000)) (ldec (0.3944753400)) (ldec (857.4857700000)) (-997) (-993) (-115) (-85) (-1185) (-719) (-1163) (-715),
  Result False (ldec (41.7774900000)) (udec (47.4905500000)) (ldec (0.3971523450)) (ldec (853.3763550000)) (-991) (-987) (-109) (-77) (-1181) (-719) (-1159) (-715),
  Result False (ldec (41.5322700000)) (udec (47.2670700000)) (ldec (0.4000474700)) (ldec (849.6730650000)) (-985) (-981) (-103) (-71) (-1177) (-719) (-1155) (-715),
  Result False (ldec (41.2079100000)) (udec (47.0206600000)) (ldec (0.4060430150)) (ldec (296.9269650000)) (-979) (-975) (-97) (-67) (-1173) (-719) (-1151) (-715),
  Result False (ldec (40.9505500000)) (udec (46.7976400000)) (ldec (0.4097916200)) (ldec (295.8655300000)) (-973) (-969) (-91) (-61) (-1169) (-717) (-1147) (-713),
  Result False (ldec (40.8630100000)) (udec (46.5334200000)) (ldec (0.4139452100)) (ldec (294.4760600000)) (-967) (-963) (-85) (-55) (-1165) (-717) (-1143) (-713),
  Result False (ldec (40.6266600000)) (udec (46.2971800000)) (ldec (0.4192696750)) (ldec (293.1111950000)) (-961) (-957) (-79) (-49) (-1161) (-717) (-1137) (-713),
  Result False (ldec (40.3926800000)) (udec (46.0722500000)) (ldec (0.4218094050)) (ldec (291.7704600000)) (-955) (-951) (-73) (-43) (-1157) (-717) (-1133) (-713),
  Result False (ldec (40.1617000000)) (udec (45.8473100000)) (ldec (0.4265795450)) (ldec (290.4529050000)) (-949) (-945) (-67) (-39) (-1153) (-715) (-1129) (-713),
  Result False (ldec (39.7174300000)) (udec (45.6183600000)) (ldec (0.4294458850)) (ldec (285.0314450000)) (-943) (-939) (-63) (-33) (-1147) (-715) (-1125) (-711),
  Result False (ldec (39.4565600000)) (udec (45.3927600000)) (ldec (0.4341979750)) (ldec (283.4049500000)) (-937) (-933) (-57) (-29) (-1143) (-715) (-1121) (-711),
  Result False (ldec (39.2038200000)) (udec (45.1389000000)) (ldec (0.4373977650)) (ldec (282.1912300000)) (-931) (-927) (-51) (-21) (-1139) (-715) (-1117) (-711),
  Result False (ldec (38.9514200000)) (udec (44.9355600000)) (ldec (0.4419108350)) (ldec (280.9976500000)) (-925) (-921) (-45) (-17) (-1135) (-715) (-1111) (-709),
  Result False (ldec (38.8318300000)) (udec (44.7080500000)) (ldec (0.4460919750)) (ldec (279.8236400000)) (-919) (-915) (-39) (-11) (-1131) (-713) (-1107) (-709),
  Result False (ldec (38.2878400000)) (udec (44.5038600000)) (ldec (0.4484330600)) (ldec (137.4043900000)) (-913) (-909) (-35) (-7) (-1127) (-713) (-1103) (-709),
  Result False (ldec (38.0324100000)) (udec (44.4184200000)) (ldec (0.4498394400)) (ldec (136.8211850000)) (-907) (-903) (-29) (-1) (-1121) (-713) (-1099) (-709),
  Result False (ldec (37.8228200000)) (udec (44.3945200000)) (ldec (0.4513976300)) (ldec (136.2474800000)) (-901) (-897) (-23) 3 (-1117) (-713) (-1095) (-707),
  Result False (ldec (37.6441400000)) (udec (44.2608300000)) (ldec (0.4544281300)) (ldec (135.6835600000)) (-895) (-891) (-17) 9 (-1113) (-711) (-1089) (-707),
  Result False (ldec (37.3892700000)) (udec (44.0387200000)) (ldec (0.4574530250)) (ldec (135.1281900000)) (-889) (-885) (-13) 15 (-1109) (-711) (-1085) (-707),
  Result False (ldec (36.9726200000)) (udec (43.8805400000)) (ldec (0.4598720100)) (ldec (132.5044800000)) (-883) (-879) (-7) 19 (-1103) (-711) (-1081) (-707),
  Result False (ldec (36.7112300000)) (udec (43.7375000000)) (ldec (0.4619792050)) (ldec (131.8649400000)) (-877) (-873) (-3) 25 (-1099) (-711) (-1077) (-705),
  Result False (ldec (36.4507600000)) (udec (43.5182900000)) (ldec (0.4665356900)) (ldec (131.3541250000)) (-871) (-867) 3 29 (-1095) (-709) (-1071) (-705),
  Result False (ldec (36.2984800000)) (udec (43.2963700000)) (ldec (0.4693489250)) (ldec (130.8510050000)) (-865) (-861) 7 35 (-1091) (-709) (-1067) (-705),
  Result False (ldec (35.9467700000)) (udec (42.8265100000)) (ldec (0.4771386400)) (ldec (130.3553900000)) (-859) (-855) 13 39 (-1085) (-709) (-1063) (-705),
  Result False (ldec (35.8471400000)) (udec (42.7023000000)) (ldec (0.4807718200)) (ldec (91.4538400000)) (-853) (-849) 19 43 (-1081) (-707) (-1059) (-703),
  Result False (ldec (36.0368300000)) (udec (42.4748700000)) (ldec (0.4859980550)) (ldec (82.7223900000)) (-847) (-843) 23 49 (-1077) (-707) (-1055) (-703),
  Result False (ldec (35.7036800000)) (udec (42.2571600000)) (ldec (0.4886019100)) (ldec (79.2771200000)) (-841) (-837) 27 53 (-1071) (-707) (-1049) (-703),
  Result False (ldec (35.4705000000)) (udec (42.0830800000)) (ldec (0.4915031150)) (ldec (78.9555450000)) (-835) (-831) 33 59 (-1067) (-707) (-1045) (-703),
  Result False (ldec (35.3731900000)) (udec (41.9525600000)) (ldec (0.4955868800)) (ldec (78.5669950000)) (-829) (-825) 37 63 (-1063) (-705) (-1041) (-701),
  Result False (ldec (34.7623200000)) (udec (41.7460800000)) (ldec (0.4996187750)) (ldec (77.1944350000)) (-823) (-819) 43 67 (-1057) (-705) (-1035) (-701),
  Result False (ldec (34.5273600000)) (udec (41.5398300000)) (ldec (0.5028187550)) (ldec (64.9632800000)) (-817) (-813) 47 71 (-1053) (-705) (-1031) (-701),
  Result False (ldec (34.2895900000)) (udec (41.3164000000)) (ldec (0.5072962000)) (ldec (64.7325250000)) (-811) (-807) 51 77 (-1049) (-705) (-1025) (-699),
  Result False (ldec (34.2557700000)) (udec (41.0951700000)) (ldec (0.5123302500)) (ldec (55.8616530000)) (-805) (-801) 57 81 (-1043) (-703) (-1021) (-699),
  Result False (ldec (33.9718800000)) (udec (40.8311100000)) (ldec (0.5175644650)) (ldec (55.6152515000)) (-799) (-795) 63 87 (-1039) (-703) (-1017) (-699),
  Result False (ldec (33.9136700000)) (udec (40.6096300000)) (ldec (0.5205684600)) (ldec (54.7552450000)) (-793) (-789) 67 91 (-1035) (-703) (-1011) (-699),
  Result False (ldec (33.7311400000)) (udec (40.3168500000)) (ldec (0.5268043550)) (ldec (41.0045935000)) (-787) (-783) 71 95 (-1029) (-701) (-1007) (-697),
  Result False (ldec (33.7311400000)) (udec (40.1919000000)) (ldec (0.5306770300)) (ldec (39.5759075000)) (-781) (-777) 75 99 (-1025) (-701) (-1003) (-697),
  Result False (ldec (34.0576100000)) (udec (39.6449900000)) (ldec (0.5401755100)) (ldec (39.4307855000)) (-775) (-771) 81 105 (-1019) (-701) (-997) (-697),
  Result False (ldec (33.8897800000)) (udec (39.4485000000)) (ldec (0.5457058400)) (ldec (39.2403865000)) (-769) (-765) 85 109 (-1015) (-699) (-993) (-695),
  Result False (ldec (33.7028000000)) (udec (39.2120300000)) (ldec (0.5507726650)) (ldec (37.2738010000)) (-763) (-759) 91 113 (-1011) (-699) (-989) (-695),
  Result False (ldec (33.5090300000)) (udec (38.9882300000)) (ldec (0.5540409500)) (ldec (37.1159870000)) (-757) (-753) 95 117 (-1005) (-699) (-983) (-695),
  Result False (ldec (33.3119300000)) (udec (38.8861200000)) (ldec (0.5567199500)) (ldec (36.9441985000)) (-751) (-747) 97 121 (-1001) (-699) (-979) (-693),
  Result False (ldec (32.9862900000)) (udec (38.6494000000)) (ldec (0.5610975500)) (ldec (36.8152170000)) (-745) (-741) 103 125 (-995) (-697) (-975) (-693),
  Result False (ldec (32.9114200000)) (udec (38.4761000000)) (ldec (0.5635091250)) (ldec (36.6878410000)) (-739) (-735) 107 131 (-991) (-697) (-969) (-693),
  Result False (ldec (32.4465900000)) (udec (38.2381000000)) (ldec (0.5683423450)) (ldec (32.8711305000)) (-733) (-729) 113 135 (-985) (-697) (-963) (-691),
  Result False (ldec (32.3727000000)) (udec (38.0646400000)) (ldec (0.5735704800)) (ldec (32.3902975000)) (-727) (-723) 117 139 (-981) (-695) (-959) (-691),
  Result False (ldec (32.3497500000)) (udec (37.8805400000)) (ldec (0.5773732350)) (ldec (23.9679585000)) (-721) (-717) 121 143 (-975) (-695) (-953) (-691),
  Result False (ldec (32.1664700000)) (udec (37.6716100000)) (ldec (0.5795357200)) (ldec (22.4237145000)) (-715) (-711) 125 147 (-971) (-695) (-949) (-691),
  Result False (ldec (31.9835700000)) (udec (37.5102600000)) (ldec (0.5845834500)) (ldec (22.3501180000)) (-709) (-705) 129 151 (-965) (-693) (-943) (-689),
  Result False (ldec (31.8084200000)) (udec (37.3250200000)) (ldec (0.5885205350)) (ldec (22.2534080000)) (-703) (-699) 133 155 (-961) (-693) (-939) (-689),
  Result False (ldec (31.6210800000)) (udec (37.1581400000)) (ldec (0.5912500750)) (ldec (22.1819205000)) (-697) (-693) 137 159 (-955) (-693) (-935) (-689),
  Result False (ldec (31.4413500000)) (udec (36.9656700000)) (ldec (0.5947969000)) (ldec (22.1112975000)) (-691) (-687) 141 163 (-951) (-691) (-929) (-687),
  Result False (ldec (31.2692400000)) (udec (36.7553300000)) (ldec (0.5999601500)) (ldec (22.0415295000)) (-685) (-681) 147 167 (-945) (-691) (-925) (-687),
  Result False (ldec (31.0753400000)) (udec (36.5920100000)) (ldec (0.6026780050)) (ldec (21.9498260000)) (-679) (-675) 149 171 (-941) (-691) (-919) (-687),
  Result False (ldec (30.8924400000)) (udec (36.4140700000)) (ldec (0.6067621500)) (ldec (16.0162590000)) (-673) (-669) 153 175 (-935) (-689) (-915) (-685),
  Result False (ldec (30.7239400000)) (udec (36.2372100000)) (ldec (0.6111772750)) (ldec (15.8901750000)) (-667) (-663) 157 179 (-929) (-689) (-909) (-685),
  Result False (ldec (30.5945700000)) (udec (36.0137700000)) (ldec (0.6162138900)) (ldec (15.6692620000)) (-661) (-657) 163 181 (-925) (-687) (-905) (-685),
  Result False (ldec (30.4080200000)) (udec (35.8244900000)) (ldec (0.6198366200)) (ldec (15.1892650000)) (-655) (-651) 167 185 (-919) (-687) (-899) (-683),
  Result False (ldec (30.1837800000)) (udec (35.6450100000)) (ldec (0.6225018450)) (ldec (15.1606700000)) (-649) (-645) 171 191 (-915) (-687) (-895) (-683),
  Result False (ldec (30.0127600000)) (udec (35.4806600000)) (ldec (0.6284368750)) (ldec (15.1047720000)) (-643) (-639) 175 195 (-909) (-685) (-889) (-681),
  Result False (ldec (29.8616600000)) (udec (35.2922600000)) (ldec (0.6313892850)) (ldec (15.0245635000)) (-637) (-633) 179 197 (-903) (-685) (-883) (-681),
  Result False (ldec (29.6896000000)) (udec (35.1015100000)) (ldec (0.6372207650)) (ldec (14.9980395000)) (-631) (-627) 183 201 (-899) (-685) (-877) (-681),
  Result False (ldec (29.5086900000)) (udec (35.0051400000)) (ldec (0.6392882500)) (ldec (14.9459130000)) (-625) (-621) 185 205 (-893) (-683) (-873) (-679),
  Result False (ldec (29.3449100000)) (udec (34.8214300000)) (ldec (0.6459882200)) (ldec (14.9203675000)) (-619) (-615) 189 209 (-889) (-683) (-867) (-679),
  Result False (ldec (29.1598300000)) (udec (34.6462300000)) (ldec (0.6514646850)) (ldec (14.9203675000)) (-613) (-609) 193 213 (-883) (-681) (-863) (-679),
  Result False (ldec (28.9866100000)) (udec (34.4583600000)) (ldec (0.6548386100)) (ldec (14.8810660000)) (-607) (-603) 197 217 (-877) (-681) (-857) (-677),
  Result False (ldec (28.8668500000)) (udec (34.2674900000)) (ldec (0.6559391850)) (ldec (14.8443770000)) (-601) (-597) 201 219 (-871) (-681) (-851) (-677),
  Result False (ldec (28.6728200000)) (udec (34.1160700000)) (ldec (0.6584395850)) (ldec (11.2899900000)) (-595) (-591) 205 223 (-867) (-679) (-847) (-675),
  Result False (ldec (28.4809200000)) (udec (33.9159500000)) (ldec (0.6660238150)) (ldec (10.6202495000)) (-589) (-585) 209 227 (-861) (-679) (-841) (-675),
  Result False (ldec (28.3295100000)) (udec (33.7294900000)) (ldec (0.6732842850)) (ldec (10.5652065000)) (-583) (-579) 213 231 (-857) (-679) (-837) (-675),
  Result False (ldec (28.1467000000)) (udec (33.6093300000)) (ldec (0.6765083000)) (ldec (10.5380745000)) (-577) (-573) 215 235 (-851) (-677) (-831) (-673),
  Result False (ldec (28.0184900000)) (udec (33.4536800000)) (ldec (0.6803448750)) (ldec (10.5111990000)) (-571) (-567) 219 237 (-845) (-677) (-825) (-673),
  Result False (ldec (27.8405300000)) (udec (33.2554100000)) (ldec (0.6860936100)) (ldec (10.4845800000)) (-565) (-561) 223 241 (-839) (-675) (-819) (-671),
  Result False (ldec (27.6617800000)) (udec (33.0644700000)) (ldec (0.6914397350)) (ldec (8.0911405000)) (-559) (-555) 227 245 (-835) (-675) (-815) (-671),
  Result False (ldec (27.5498600000)) (udec (32.9341800000)) (ldec (0.6945606750)) (ldec (7.6262485000)) (-553) (-549) 231 247 (-829) (-675) (-809) (-671),
  Result False (ldec (27.3484100000)) (udec (32.7880900000)) (ldec (0.6984887350)) (ldec (7.6073625000)) (-547) (-543) 233 251 (-823) (-673) (-803) (-669),
  Result False (ldec (27.1894300000)) (udec (32.6062900000)) (ldec (0.7018282700)) (ldec (7.5886465500)) (-541) (-537) 237 255 (-817) (-673) (-797) (-669),
  Result False (ldec (27.0150800000)) (udec (32.4549500000)) (ldec (0.7061610300)) (ldec (7.5636568000)) (-535) (-531) 241 259 (-811) (-671) (-791) (-667),
  Result False (ldec (26.9112200000)) (udec (32.2865400000)) (ldec (0.7129850700)) (ldec (7.5335057000)) (-529) (-525) 245 261 (-807) (-671) (-787) (-667),
  Result False (ldec (26.7148300000)) (udec (32.0709200000)) (ldec (0.7181159250)) (ldec (7.5154547500)) (-523) (-519) 249 265 (-801) (-669) (-781) (-665),
  Result False (ldec (26.5463800000)) (udec (31.9688000000)) (ldec (0.7198401750)) (ldec (7.4975643500)) (-517) (-513) 251 269 (-795) (-669) (-775) (-665),
  Result False (ldec (26.4216700000)) (udec (31.8122000000)) (ldec (0.7257524050)) (ldec (7.4916468000)) (-511) (-507) 255 271 (-789) (-669) (-769) (-665),
  Result False (ldec (26.2472300000)) (udec (31.8342500000)) (ldec (0.7275730800)) (ldec (5.7500982500)) (-505) (-501) 257 275 (-783) (-667) (-763) (-663),
  Result False (ldec (26.1145800000)) (udec (31.8342500000)) (ldec (0.7356626150)) (ldec (5.7290909000)) (-499) (-495) 261 277 (-777) (-667) (-757) (-663),
  Result False (ldec (25.9287200000)) (udec (31.7691800000)) (ldec (0.7405023900)) (ldec (5.7083628500)) (-493) (-489) 265 281 (-773) (-665) (-753) (-661),
  Result False (ldec (25.6335800000)) (udec (31.5782600000)) (ldec (0.7428558250)) (ldec (5.6879093500)) (-487) (-483) 267 285 (-767) (-665) (-747) (-661),
  Result False (ldec (25.6533300000)) (udec (31.4503000000)) (ldec (0.7481921650)) (ldec (5.6828230500)) (-481) (-477) 271 287 (-761) (-663) (-741) (-659),
  Result False (ldec (25.0111800000)) (udec (31.2596600000)) (ldec (0.7522282400)) (ldec (5.6132146500)) (-475) (-471) 275 291 (-755) (-663) (-735) (-659),
  Result False (ldec (24.8099500000)) (udec (31.1970300000)) (ldec (0.7587517000)) (ldec (5.5934489500)) (-469) (-465) 277 293 (-749) (-661) (-729) (-657),
  Result False (ldec (24.6117200000)) (udec (31.0094600000)) (ldec (0.7630674550)) (ldec (5.5743824500)) (-463) (-459) 281 297 (-743) (-661) (-723) (-657),
  Result False (ldec (24.4136500000)) (udec (30.5842100000)) (ldec (0.7671694600)) (ldec (5.5555534500)) (-457) (-453) 285 301 (-737) (-659) (-717) (-655),
  Result False (ldec (24.3835200000)) (udec (30.4231000000)) (ldec (0.7709441900)) (ldec (5.5516100000)) (-451) (-447) 287 303 (-731) (-659) (-711) (-655),
  Result False (ldec (24.3835200000)) (udec (30.5729800000)) (ldec (0.7755399100)) (ldec (5.5015735000)) (-445) (-441) 291 307 (-725) (-657) (-705) (-653),
  Result False (ldec (24.2787500000)) (udec (30.5729800000)) (ldec (0.7783875350)) (ldec (5.0429847500)) (-439) (-435) 293 309 (-719) (-657) (-699) (-653),
  Result False (ldec (24.0867700000)) (udec (30.5160200000)) (ldec (0.7862168650)) (ldec (4.9778328000)) (-433) (-429) 297 313 (-713) (-655) (-693) (-651),
  Result False (ldec (23.8949400000)) (udec (30.3338300000)) (ldec (0.7909994500)) (ldec (4.9178184500)) (-427) (-423) 299 315 (-707) (-655) (-687) (-651),
  Result False (ldec (23.7032400000)) (udec (30.1517700000)) (ldec (0.7953983300)) (ldec (4.9062588500)) (-421) (-417) 303 319 (-701) (-653) (-681) (-649),
  Result False (ldec (23.5116800000)) (udec (30.0246300000)) (ldec (0.8027364150)) (ldec (4.8947980500)) (-415) (-411) 307 321 (-695) (-653) (-675) (-649),
  Result False (ldec (23.4854700000)) (udec (29.8420900000)) (ldec (0.8047942100)) (ldec (4.8834351000)) (-409) (-405) 309 325 (-689) (-651) (-669) (-647),
  Result False (ldec (23.3202300000)) (udec (29.7880300000)) (ldec (0.8144295850)) (ldec (4.8721681000)) (-403) (-399) 313 327 (-683) (-651) (-663) (-647),
  Result False (ldec (23.1288900000)) (udec (29.6063300000)) (ldec (0.8182390850)) (ldec (4.8499181500)) (-397) (-393) 315 329 (-677) (-649) (-657) (-645),
  Result False (ldec (23.1043200000)) (udec (29.4247200000)) (ldec (0.8229831000)) (ldec (4.8199390000)) (-391) (-387) 319 333 (-671) (-649) (-651) (-645),
  Result False (ldec (23.1043200000)) (udec (29.2432100000)) (ldec (0.8232012200)) (ldec (4.1345548500)) (-385) (-381) 321 337 (-665) (-647) (-643) (-643),
  Result False (ldec (23.1592900000)) (udec (28.4905000000)) (ldec (0.8329163950)) (ldec (4.1179669000)) (-379) (-375) 325 339 (-659) (-647) (-639) (-641),
  Result False (ldec (23.0311000000)) (udec (28.3773100000)) (ldec (0.8397607650)) (ldec (4.1097617500)) (-373) (-369) 327 341 (-653) (-645) (-631) (-641),
  Result False (ldec (22.9062300000)) (udec (28.2569400000)) (ldec (0.8449185050)) (ldec (4.1016155000)) (-367) (-363) 329 345 (-647) (-645) (-625) (-639),
  Result False (ldec (22.7854300000)) (udec (28.0943200000)) (ldec (0.8469915000)) (ldec (4.0854949500)) (-361) (-357) 333 347 (-639) (-643) (-619) (-639),
  Result False (ldec (22.6117900000)) (udec (27.9703300000)) (ldec (0.8546169600)) (ldec (4.0775159000)) (-355) (-351) 335 351 (-633) (-643) (-611) (-637),
  Result False (ldec (22.4893000000)) (udec (27.7986600000)) (ldec (0.8615698200)) (ldec (3.0552522500)) (-349) (-345) 339 353 (-627) (-641) (-605) (-635),
  Result False (ldec (22.3420700000)) (udec (27.6944200000)) (ldec (0.8676389900)) (ldec (3.0465673500)) (-343) (-339) 341 355 (-621) (-639) (-599) (-635),
  Result False (ldec (22.2150800000)) (udec (27.5214600000)) (ldec (0.8753078650)) (ldec (3.0449647000)) (-337) (-333) 345 359 (-615) (-639) (-593) (-633),
  Result False (ldec (22.0932300000)) (udec (27.4155400000)) (ldec (0.8802476750)) (ldec (3.0379860000)) (-331) (-327) 347 361 (-607) (-637) (-587) (-633),
  Result False (ldec (21.9473800000)) (udec (27.2313600000)) (ldec (0.8861404300)) (ldec (3.0295063000)) (-325) (-321) 351 365 (-601) (-637) (-579) (-631),
  Result False (ldec (21.8104900000)) (udec (27.1436200000)) (ldec (0.8908298200)) (ldec (3.0280205000)) (-319) (-315) 353 367 (-595) (-635) (-573) (-629),
  Result False (ldec (21.2323600000)) (udec (27.7480800000)) (ldec (0.8959602000)) (ldec (2.9057754500)) (-313) (-309) 355 369 (-587) (-633) (-567) (-629),
  Result False (ldec (21.2500000000)) (udec (27.7480800000)) (ldec (0.8823070300)) (ldec (2.9053254000)) (-307) (-303) 359 373 (-581) (-633) (-559) (-627),
  Result False (ldec (20.7677300000)) (udec (27.6987600000)) (ldec (0.9071218450)) (ldec (2.8840318500)) (-301) (-297) 361 375 (-575) (-631) (-553) (-625),
  Result False (ldec (20.7548000000)) (udec (27.4831900000)) (ldec (0.9131654600)) (ldec (2.8832215000)) (-295) (-291) 363 377 (-567) (-629) (-545) (-625),
  Result False (ldec (20.5351800000)) (udec (27.3152800000)) (ldec (0.9243062050)) (ldec (2.8733662000)) (-289) (-285) 367 379 (-561) (-629) (-539) (-623),
  Result False (ldec (20.5231600000)) (udec (27.2675300000)) (ldec (0.9278804850)) (ldec (2.8726176000)) (-283) (-279) 369 383 (-555) (-627) (-533) (-621),
  Result False (ldec (20.5231600000)) (udec (27.0517700000)) (ldec (0.9360392750)) (ldec (2.8726176000)) (-277) (-273) 371 385 (-547) (-625) (-525) (-621),
  Result False (ldec (20.7737300000)) (udec (26.0714200000)) (ldec (0.9421657300)) (ldec (3.6400029000)) (-271) (-267) 375 389 (-541) (-625) (-519) (-619),
  Result False (ldec (20.6691700000)) (udec (25.9875700000)) (ldec (0.9478185150)) (ldec (3.6318091500)) (-265) (-261) 377 391 (-533) (-623) (-511) (-617),
  Result False (ldec (20.5553100000)) (udec (25.8499500000)) (ldec (0.9592207000)) (ldec (3.6236857000)) (-259) (-255) 379 393 (-527) (-621) (-503) (-615),
  Result False (ldec (20.4226000000)) (udec (25.6907700000)) (ldec (0.9657472000)) (ldec (3.4426252000)) (-253) (-249) 383 395 (-519) (-621) (-497) (-615),
  Result False (ldec (20.2787400000)) (udec (25.5702500000)) (ldec (0.9722281000)) (ldec (3.4357671500)) (-247) (-243) 385 399 (-513) (-619) (-489) (-613),
  Result False (ldec (20.1623500000)) (udec (25.4975800000)) (ldec (0.9832595000)) (ldec (3.4279543500)) (-241) (-237) 387 401 (-505) (-617) (-483) (-611),
  Result False (ldec (20.0582200000)) (udec (25.3697400000)) (ldec (0.9896625000)) (ldec (3.4212283500)) (-235) (-231) 389 403 (-499) (-617) (-475) (-609),
  Result False (ldec (19.9586900000)) (udec (25.2101500000)) (ldec (1.0019099000)) (ldec (3.1782468500)) (-229) (-225) 393 405 (-491) (-615) (-469) (-609),
  Result False (ldec (19.8271800000)) (udec (25.0970200000)) (ldec (1.0095545500)) (ldec (3.1721877500)) (-223) (-219) 395 407 (-483) (-613) (-461) (-607),
  Result False (ldec (19.7185300000)) (udec (24.9891600000)) (ldec (1.0184855000)) (ldec (3.1661714000)) (-217) (-213) 397 409 (-477) (-611) (-453) (-605),
  Result False (ldec (19.5664800000)) (udec (24.8271900000)) (ldec (1.0249607000)) (ldec (3.1601978000)) (-211) (-207) 401 413 (-469) (-609) (-447) (-603),
  Result False (ldec (19.4557300000)) (udec (24.7156400000)) (ldec (1.0349794000)) (ldec (3.0005398500)) (-205) (-201) 403 415 (-461) (-609) (-439) (-601),
  Result False (ldec (19.3472000000)) (udec (24.6040900000)) (ldec (1.0405464000)) (ldec (2.9951277000)) (-199) (-195) 405 417 (-455) (-607) (-431) (-601),
  Result False (ldec (19.2380800000)) (udec (24.5079700000)) (ldec (1.0488617500)) (ldec (2.9897516500)) (-193) (-189) 407 419 (-447) (-605) (-423) (-599),
  Result False (ldec (19.1341800000)) (udec (24.3422900000)) (ldec (1.0637948000)) (ldec (2.9837894500)) (-187) (-183) 411 421 (-439) (-603) (-415) (-597),
  Result False (ldec (19.0001600000)) (udec (24.2547500000)) (ldec (1.0711554000)) (ldec (2.8534390000)) (-181) (-177) 413 423 (-431) (-601) (-407) (-595),
  Result False (ldec (18.8741800000)) (udec (24.1273400000)) (ldec (1.0809964500)) (ldec (2.8487887500)) (-175) (-171) 415 427 (-423) (-601) (-401) (-593),
  Result False (ldec (18.7663000000)) (udec (24.0281100000)) (ldec (1.0876702000)) (ldec (2.8401067000)) (-169) (-165) 417 429 (-415) (-599) (-393) (-591),
  Result False (ldec (18.6462800000)) (udec (23.8453400000)) (ldec (1.0996858000)) (ldec (2.7290146500)) (-163) (-159) 421 431 (-407) (-597) (-385) (-589),
  Result False (ldec (18.5480500000)) (udec (23.7804000000)) (ldec (1.1075299500)) (ldec (2.7248052000)) (-157) (-153) 423 433 (-399) (-595) (-377) (-589),
  Result False (ldec (18.4567400000)) (udec (23.6409200000)) (ldec (1.1293533500)) (ldec (2.7201549500)) (-151) (-147) 425 435 (-391) (-593) (-369) (-587),
  Result False (ldec (18.3298800000)) (udec (23.5480600000)) (ldec (1.1344216000)) (ldec (2.7123174500)) (-145) (-141) 427 437 (-383) (-591) (-361) (-585),
  Result False (ldec (18.2237300000)) (udec (23.4464800000)) (ldec (1.1438218500)) (ldec (2.6139848500)) (-139) (-135) 429 439 (-375) (-589) (-351) (-583),
  Result False (ldec (18.1062100000)) (udec (23.2658600000)) (ldec (1.1602141000)) (ldec (2.6103283000)) (-133) (-129) 433 441 (-367) (-587) (-343) (-581),
  Result False (ldec (17.9970100000)) (udec (23.1789600000)) (ldec (1.1689094500)) (ldec (2.6066888500)) (-127) (-123) 435 445 (-359) (-585) (-335) (-579),
  Result False (ldec (17.8667600000)) (udec (23.0839600000)) (ldec (1.1851193000)) (ldec (2.5465529000)) (-121) (-117) 437 447 (-351) (-583) (-327) (-577),
  Result False (ldec (17.7537200000)) (udec (22.9613900000)) (ldec (1.1959065500)) (ldec (2.5422513000)) (-115) (-111) 439 449 (-341) (-581) (-319) (-575),
  Result False (ldec (17.6288700000)) (udec (22.8671500000)) (ldec (1.2064857500)) (ldec (2.5376580500)) (-109) (-105) 441 451 (-333) (-579) (-309) (-573),
  Result False (ldec (17.5307900000)) (udec (22.7608600000)) (ldec (1.2268081500)) (ldec (2.4188263500)) (-103) (-99) 443 453 (-325) (-577) (-301) (-569),
  Result False (ldec (17.4468500000)) (udec (22.6491500000)) (ldec (1.2388912000)) (ldec (2.4147974000)) (-97) (-93) 445 455 (-317) (-575) (-291) (-567),
  Result False (ldec (17.3279500000)) (udec (22.5509300000)) (ldec (1.2509115500)) (ldec (2.4108995500)) (-91) (-87) 447 457 (-309) (-573) (-283) (-565),
  Result False (ldec (17.2180100000)) (udec (22.4528100000)) (ldec (1.2722248000)) (ldec (2.3463869500)) (-85) (-81) 449 459 (-299) (-571) (-273) (-563),
  Result False (ldec (17.0897900000)) (udec (22.3472900000)) (ldec (1.2813771000)) (ldec (2.3425831500)) (-79) (-75) 451 463 (-291) (-569) (-265) (-561),
  Result False (ldec (16.9919100000)) (udec (22.2419600000)) (ldec (1.2949687500)) (ldec (2.3166586000)) (-73) (-69) 453 465 (-281) (-565) (-255) (-559),
  Result False (ldec (16.8914600000)) (udec (22.0692100000)) (ldec (1.3128667500)) (ldec (2.2543148500)) (-67) (-63) 457 467 (-271) (-563) (-245) (-555),
  Result False (ldec (16.7918100000)) (udec (21.9604200000)) (ldec (1.3392235500)) (ldec (2.2506393000)) (-61) (-57) 459 469 (-263) (-561) (-235) (-553),
  Result False (ldec (16.6760500000)) (udec (21.8537000000)) (ldec (1.3542316500)) (ldec (2.1835104000)) (-55) (-51) 461 471 (-253) (-559) (-225) (-551),
  Result False (ldec (16.5806600000)) (udec (21.7708100000)) (ldec (1.3692179000)) (ldec (2.1800562000)) (-49) (-45) 463 473 (-243) (-557) (-215) (-547),
  Result False (ldec (16.4793900000)) (udec (21.6742700000)) (ldec (1.3856880500)) (ldec (2.1766191000)) (-43) (-39) 465 475 (-233) (-553) (-205) (-545),
  Result False (ldec (16.3798800000)) (udec (21.5806700000)) (ldec (1.4124989500)) (ldec (2.1095215500)) (-37) (-33) 467 477 (-223) (-551) (-195) (-543),
  Result False (ldec (16.2820300000)) (udec (21.4794000000)) (ldec (1.4307332500)) (ldec (2.1058849500)) (-31) (-27) 469 479 (-213) (-549) (-187) (-539),
  Result False (ldec (16.1857900000)) (udec (21.3798900000)) (ldec (1.4478855000)) (ldec (2.1027832000)) (-25) (-21) 471 481 (-203) (-545) (-177) (-537),
  Result False (ldec (16.0658300000)) (udec (21.2820400000)) (ldec (1.4807764000)) (ldec (2.0580135000)) (-19) (-15) 473 483 (-193) (-543) (-165) (-533),
  Result False (ldec (15.9645000000)) (udec (21.1858000000)) (ldec (1.5002485500)) (ldec (2.0545004000)) (-13) (-9) 475 485 (-183) (-541) (-155) (-531),
  Result False (ldec (15.8817700000)) (udec (21.0658400000)) (ldec (1.5218439500)) (ldec (1.9945601500)) (-7) (-3) 477 487 (-173) (-537) (-143) (-527),
  Result False (ldec (15.7672400000)) (udec (20.9843900000)) (ldec (1.5556630000)) (ldec (1.9912893000)) (-1) 3 479 489 (-163) (-535) (-133) (-525),
  Result False (ldec (15.6712300000)) (udec (20.8817800000)) (ldec (1.5774949500)) (ldec (1.9540217500)) 5 9 481 491 (-151) (-531) (-121) (-521),
  Result False (ldec (15.5776800000)) (udec (20.7918500000)) (ldec (1.6011642000)) (ldec (1.9514007000)) 11 15 483 493 (-141) (-527) (-109) (-517),
  Result False (ldec (15.4760900000)) (udec (20.6710500000)) (ldec (1.6533097000)) (ldec (1.9479218000)) 17 21 485 495 (-129) (-525) (-97) (-513),
  Result False (ldec (15.3754400000)) (udec (20.5844500000)) (ldec (1.6776705500)) (ldec (1.8934782500)) 23 27 487 497 (-117) (-521) (-85) (-511),
  Result False (ldec (15.2751400000)) (udec (20.4761000000)) (ldec (1.7206466500)) (ldec (1.8902815000)) 29 33 489 499 (-105) (-517) (-73) (-507),
  Result False (ldec (15.1979500000)) (udec (20.3921100000)) (ldec (1.7638260500)) (ldec (1.8547306000)) 35 39 491 499 (-95) (-515) (-61) (-503),
  Result False (ldec (15.0964000000)) (udec (20.2792600000)) (ldec (1.7941738000)) (ldec (1.8523926500)) 41 45 493 501 (-83) (-511) (-47) (-499),
  Result False (ldec (15.0175600000)) (udec (20.1979600000)) (ldec (1.8446577500)) (ldec (1.8040680500)) 47 51 495 503 (-69) (-507) (-35) (-495),
  Result False (ldec (14.9115000000)) (udec (20.0964100000)) (ldec (1.8831451000)) (ldec (1.8012256500)) 53 57 497 505 (-57) (-503) (-21) (-489),
  Result False (ldec (14.8143100000)) (udec (19.9889700000)) (ldec (1.9410210000)) (ldec (1.7739084000)) 59 63 499 507 (-45) (-499) (-7) (-485),
  Result False (ldec (14.7390600000)) (udec (19.8909100000)) (ldec (1.9815736500)) (ldec (1.7712047000)) 65 69 501 509 (-29) (-493) 7 (-481),
  Result False (ldec (14.6377300000)) (udec (19.7866700000)) (ldec (2.0450412500)) (ldec (1.7312268000)) 71 75 503 511 (-15) (-489) 21 (-475),
  Result False (ldec (14.5452000000)) (udec (19.6918300000)) (ldec (2.0945799500)) (ldec (1.7283882000)) 77 81 505 513 (-1) (-485) 37 (-471),
  Result False (ldec (14.4470300000)) (udec (19.5913000000)) (ldec (2.1658138000)) (ldec (1.6868295000)) 83 87 507 515 13 (-481) 55 (-465),
  Result False (ldec (14.3518000000)) (udec (19.4994700000)) (ldec (2.2379036000)) (ldec (1.6848563500)) 89 93 509 517 27 (-475) 71 (-459),
  Result False (ldec (14.2508600000)) (udec (19.4020400000)) (ldec (2.3048121000)) (ldec (1.6627090000)) 95 99 511 519 43 (-469) 85 (-453),
  Result False (ldec (14.1554400000)) (udec (19.2876000000)) (ldec (2.3974171500)) (ldec (1.6601896000)) 101 105 513 521 59 (-465) 103 (-447),
  Result False (ldec (14.0826900000)) (udec (19.1933900000)) (ldec (2.5237434000)) (ldec (1.6096391500)) 107 111 515 521 75 (-459) 121 (-439),
  Result False (ldec (14.0038100000)) (udec (19.1711700000)) (ldec (2.5923125000)) (ldec (1.6073696000)) 113 117 515 523 93 (-451) 141 (-433),
  Result False (ldec (13.9138900000)) (udec (19.0707900000)) (ldec (2.6996330500)) (ldec (1.5854635500)) 119 123 517 525 111 (-445) 161 (-425),
  Result False (ldec (13.8178300000)) (udec (18.9795800000)) (ldec (2.8214563000)) (ldec (1.5831778500)) 125 129 519 527 133 (-437) 181 (-417),
  Result False (ldec (13.7368600000)) (udec (18.8900000000)) (ldec (2.9628476500)) (ldec (1.5632430500)) 131 135 521 529 153 (-431) 205 (-407),
  Result False (ldec (13.6366400000)) (udec (18.8007100000)) (ldec (3.1360412000)) (ldec (1.5610704000)) 137 141 523 531 173 (-423) 229 (-397),
  Result False (ldec (13.5492600000)) (udec (18.6967900000)) (ldec (3.3948145500)) (ldec (1.5285186500)) 143 147 525 531 195 (-413) 255 (-387),
  Result False (ldec (13.4717400000)) (udec (18.5884100000)) (ldec (3.5986617500)) (ldec (1.5264600000)) 149 153 527 533 219 (-403) 287 (-373),
  Result False (ldec (13.3891000000)) (udec (18.5015300000)) (ldec (3.8151525000)) (ldec (1.5065755500)) 155 159 529 535 243 (-393) 317 (-359),
  Result False (ldec (13.2917700000)) (udec (18.3891100000)) (ldec (4.3201962500)) (ldec (1.5046233000)) 161 165 531 537 275 (-379) 353 (-343),
  Result False (ldec (13.2114600000)) (udec (18.2917800000)) (ldec (4.7365841000)) (ldec (1.4866787500)) 167 171 533 539 305 (-365) 391 (-323),
  Result False (ldec (13.1237700000)) (udec (18.2728400000)) (ldec (4.8564247000)) (ldec (1.4544908500)) 173 177 533 541 341 (-349) 441 (-299),
  Result False (ldec (13.0289700000)) (udec (18.1959900000)) (ldec (5.3767017000)) (ldec (1.4525975000)) 179 183 535 543 381 (-331) 503 (-267),
  Result False (ldec (12.9708900000)) (udec (18.0816600000)) (ldec (7.6098230000)) (ldec (1.4369434000)) 185 189 537 543 427 (-307) 593 (-215),
  Result False (ldec (12.8814700000)) (udec (17.9725100000)) (ldec (11.0812465000)) (ldec (1.4351659500)) 191 195 539 545 (-1125) (-275) 1129 239,
  Result True (ldec (12.8042600000)) (udec (17.8814800000)) (ldec (19.0000000000)) (ldec (1.4179206000)) 197 201 541 547 (-1127) (-239) 1129 239,
  Result False (ldec (12.7175400000)) (udec (17.7717200000)) (ldec (10.5962335000)) (ldec (1.3912902000)) 203 207 543 549 (-813) 63 (-485) 277,
  Result False (ldec (12.6093600000)) (udec (17.7717200000)) (ldec (7.2823323500)) (ldec (1.3896885000)) 209 213 543 551 (-587) 217 (-425) 309,
  Result False (ldec (12.5438600000)) (udec (17.6835300000)) (ldec (5.5751215500)) (ldec (1.3749312000)) 215 219 545 551 (-497) 269 (-379) 331,
  Result False (ldec (12.4724900000)) (udec (17.5771500000)) (ldec (4.7439998000)) (ldec (1.3724735500)) 221 225 547 553 (-437) 301 (-339) 351,
  Result False (ldec (12.3883500000)) (udec (17.4725000000)) (ldec (4.0339185000)) (ldec (1.3589484000)) 227 231 549 555 (-383) 327 (-299) 369,
  Result False (ldec (12.3053000000)) (udec (17.3695400000)) (ldec (2.8726176000)) (ldec (1.3446832000)) 233 237 551 557 (-345) 347 (-269) 381,
  Result False (ldec (12.2044400000)) (udec (17.2836200000)) (ldec (3.9150269500)) (ldec (1.3431195000)) 239 243 553 559 (-311) 361 (-241) 395,
  Result False (ldec (12.1372100000)) (udec (17.2682000000)) (ldec (3.6406289500)) (ldec (1.3173593000)) 245 249 553 559 (-279) 375 (-217) 405,
  Result False (ldec (12.0722900000)) (udec (17.1836400000)) (ldec (3.4396593000)) (ldec (1.3002859000)) 251 255 555 561 (-253) 387 (-193) 413,
  Result False (ldec (11.9782100000)) (udec (17.0752500000)) (ldec (3.2408955500)) (ldec (1.2987640000)) 257 261 557 563 (-221) 401 (-169) 423,
  Result False (ldec (11.8973400000)) (udec (16.9784000000)) (ldec (3.0934745500)) (ldec (1.2858725000)) 263 267 559 565 (-199) 409 (-149) 431,
  Result False (ldec (11.8357900000)) (udec (16.9640200000)) (ldec (2.9310179000)) (ldec (1.2773377000)) 269 273 559 565 (-177) 419 (-129) 439,
  Result False (ldec (11.7562500000)) (udec (16.8655700000)) (ldec (2.8161230000)) (ldec (1.2758747000)) 275 279 561 567 (-155) 427 (-109) 447,
  Result False (ldec (11.6672100000)) (udec (16.7858100000)) (ldec (2.6899601500)) (ldec (1.2547590500)) 281 285 563 569 (-133) 435 (-91) 453,
  Result False (ldec (11.5895400000)) (udec (16.6672200000)) (ldec (2.6018704500)) (ldec (1.2534756000)) 287 291 565 571 (-113) 443 (-71) 459,
  Result False (ldec (11.4989300000)) (udec (16.5761900000)) (ldec (2.5311866500)) (ldec (1.2421677500)) 293 297 567 573 (-97) 449 (-55) 465,
  Result False (ldec (11.4258700000)) (udec (16.5611600000)) (ldec (2.4219062500)) (ldec (1.2313273000)) 299 303 567 573 (-79) 455 (-39) 471,
  Result False (ldec (11.3657900000)) (udec (16.4582700000)) (ldec (2.3385409000)) (ldec (1.2293845500)) 305 309 569 575 (-63) 461 (-21) 477,
  Result False (ldec (11.2676200000)) (udec (16.4365700000)) (ldec (2.2464707000)) (ldec (1.2094279000)) 311 315 569 577 (-45) 467 (-7) 483,
  Result False (ldec (11.1932600000)) (udec (16.3382600000)) (ldec (2.1985945000)) (ldec (1.1995308000)) 317 321 571 579 (-29) 473 7 487,
  Result False (ldec (11.1241800000)) (udec (16.2359700000)) (ldec (2.1479139000)) (ldec (1.1871352000)) 323 327 573 579 (-15) 477 23 493,
  Result False (ldec (11.0558300000)) (udec (16.1397400000)) (ldec (2.1050898000)) (ldec (1.1862479000)) 329 333 575 581 1 483 37 497,
  Result False (ldec (10.9729900000)) (udec (16.1310500000)) (ldec (2.0329287500)) (ldec (1.1705482000)) 335 339 575 583 17 489 51 501,
  Result False (ldec (10.9061900000)) (udec (16.0295800000)) (ldec (2.0065710000)) (ldec (1.1622366500)) 341 345 577 583 31 493 63 505,
  Result False (ldec (10.8478800000)) (udec (15.9319700000)) (ldec (1.9593978000)) (ldec (1.1611327500)) 347 351 579 585 43 497 77 509,
  Result False (ldec (10.7591400000)) (udec (15.8478900000)) (ldec (1.9143212500)) (ldec (1.1449248000)) 353 357 581 587 59 501 89 513,
  Result False (ldec (10.6799300000)) (udec (15.8252700000)) (ldec (1.8831983000)) (ldec (1.1359834000)) 359 363 581 589 71 505 103 517,
  Result False (ldec (10.6160300000)) (udec (15.7444700000)) (ldec (1.8357163500)) (ldec (1.1312163000)) 365 369 583 589 85 509 115 521,
  Result False (ldec (10.5384900000)) (udec (15.6406800000)) (ldec (1.8137780000)) (ldec (1.1300753500)) 371 375 585 591 99 513 127 525,
  Result False (ldec (10.4759400000)) (udec (15.5242900000)) (ldec (1.7724121500)) (ldec (1.1093216500)) 377 381 587 593 111 517 139 527,
  Result False (ldec (10.4000200000)) (udec (15.5242900000)) (ldec (1.7465018500)) (ldec (1.1014756000)) 383 387 587 593 121 521 149 531,
  Result False (ldec (10.3249700000)) (udec (15.4238800000)) (ldec (1.7280576000)) (ldec (1.0892329500)) 389 393 589 595 133 525 163 535,
  Result False (ldec (10.2643900000)) (udec (15.3249800000)) (ldec (1.6914759500)) (ldec (1.0881965000)) 395 399 591 597 147 529 173 537,
  Result False (ldec (10.1908500000)) (udec (15.3249800000)) (ldec (1.6703555500)) (ldec (1.0818486000)) 401 405 591 597 157 531 185 541,
  Result False (ldec (10.1181000000)) (udec (15.2275200000)) (ldec (1.6540972500)) (ldec (1.0730003000)) 407 411 593 599 169 535 197 543,
  Result False (ldec (10.0593700000)) (udec (15.1181100000)) (ldec (1.6229515000)) (ldec (1.0659104500)) 413 417 595 601 181 539 207 547,
  Result False (ldec (9.9880400000)) (udec (15.1181100000)) (ldec (1.6029701500)) (ldec (1.0504045500)) 419 423 595 601 191 541 217 549,
  Result False (ldec (9.9174600000)) (udec (15.0236200000)) (ldec (1.5870937500)) (ldec (1.0498241000)) 425 429 597 603 201 543 227 553,
  Result False (ldec (9.8476200000)) (udec (14.9174700000)) (ldec (1.5618731500)) (ldec (1.0418080000)) 431 435 599 605 213 547 239 555,
  Result False (ldec (9.7912200000)) (udec (14.9089800000)) (ldec (1.5425900500)) (ldec (1.0362476500)) 437 441 599 605 223 549 249 557,
  Result False (ldec (9.7226800000)) (udec (14.8129900000)) (ldec (1.5314047500)) (ldec (1.0265472000)) 443 447 601 607 235 553 257 561,
  Result False (ldec (9.6460500000)) (udec (14.7226900000)) (ldec (1.5095006000)) (ldec (1.0200245000)) 449 453 603 607 245 555 269 563,
  Result False (ldec (9.5789700000)) (udec (14.7046700000)) (ldec (1.4847635500)) (ldec (1.0194488000)) 455 459 603 609 255 557 279 565,
  Result False (ldec (9.5125500000)) (udec (14.6124300000)) (ldec (1.4745776500)) (ldec (1.0111828500)) 461 465 605 611 265 561 287 567,
  Result False (ldec (9.4467800000)) (udec (14.5003500000)) (ldec (1.4626494500)) (ldec (1.0035173000)) 467 471 607 611 275 563 299 571,
  Result False (ldec (9.3816500000)) (udec (14.5003500000)) (ldec (1.4379760500)) (ldec (0.9908804000)) 473 477 607 613 285 565 309 573,
  Result False (ldec (9.3171500000)) (udec (14.4141500000)) (ldec (1.4283687000)) (ldec (0.9845021000)) 479 483 609 615 295 569 319 575,
  Result False (ldec (9.2650300000)) (udec (14.2969600000)) (ldec (1.4147428500)) (ldec (0.9839834000)) 485 489 611 615 303 571 327 577,
  Result False (ldec (9.1969900000)) (udec (14.2969600000)) (ldec (1.4036649000)) (ldec (0.9728627000)) 491 495 611 617 313 573 337 581,
  Result False (ldec (9.1188100000)) (udec (14.2012900000)) (ldec (1.3972942000)) (ldec (0.9672387000)) 497 501 613 617 323 575 347 583,
  Result False (ldec (9.0567600000)) (udec (14.0992100000)) (ldec (1.3858942000)) (ldec (0.9601669000)) 503 507 615 619 331 577 355 585,
  Result False (ldec (8.9952800000)) (udec (14.0992100000)) (ldec (1.3749274000)) (ldec (0.9538807500)) 509 513 615 621 341 579 365 587,
  Result False (ldec (8.9417700000)) (udec (13.9873500000)) (ldec (1.3555502500)) (ldec (0.9431923000)) 515 519 617 621 351 581 373 589,
  Result False (ldec (8.8661700000)) (udec (13.9873500000)) (ldec (1.3428478000)) (ldec (0.9427274650)) 521 525 617 623 361 585 383 591,
  Result False (ldec (8.8165200000)) (udec (13.8851100000)) (ldec (1.3392834000)) (ldec (0.9366144050)) 527 531 619 623 369 587 391 593,
  Result False (ldec (8.7494200000)) (udec (13.7924600000)) (ldec (1.3319788500)) (ldec (0.9289855250)) 533 537 621 625 377 589 401 595,
  Result False (ldec (8.6904000000)) (udec (13.7893500000)) (ldec (1.3123689500)) (ldec (0.9255842400)) 539 543 621 625 387 591 409 597,
  Result False (ldec (8.6325800000)) (udec (13.6904100000)) (ldec (1.3061502500)) (ldec (0.9144987850)) 545 549 623 627 395 593 417 599,
  Result False (ldec (8.5604500000)) (udec (13.6135700000)) (ldec (1.2992922000)) (ldec (0.9084633400)) 551 555 625 629 405 595 427 601,
  Result False (ldec (8.5088000000)) (udec (13.5845600000)) (ldec (1.2914442500)) (ldec (0.9069574000)) 557 561 625 629 413 597 435 603,
  Result False (ldec (8.4339900000)) (udec (13.4907800000)) (ldec (1.2872737500)) (ldec (0.8972779450)) 563 567 627 631 421 599 443 605,
  Result False (ldec (8.3755100000)) (udec (13.4740900000)) (ldec (1.2704321500)) (ldec (0.8967156400)) 569 573 627 631 431 601 451 607,
  Result False (ldec (8.3198800000)) (udec (13.3755200000)) (ldec (1.2653914500)) (ldec (0.8917829550)) 575 579 629 633 439 603 461 609,
  Result False (ldec (8.2647000000)) (udec (13.3652000000)) (ldec (1.2546469500)) (ldec (0.8871062000)) 581 585 629 635 449 605 469 609,
  Result False (ldec (8.2029400000)) (udec (13.2647100000)) (ldec (1.2521608000)) (ldec (0.8812251300)) 587 591 631 635 457 605 477 611,
  Result False (ldec (8.1388200000)) (udec (13.1758300000)) (ldec (1.2479950500)) (ldec (0.8766398600)) 593 597 633 637 465 607 485 613,
  Result False (ldec (8.0894500000)) (udec (13.1658200000)) (ldec (1.2394944500)) (ldec (0.8677995400)) 599 603 633 637 473 609 493 615,
  Result False (ldec (8.0250300000)) (udec (13.0683600000)) (ldec (1.2284469000)) (ldec (0.8625599100)) 605 609 635 639 483 611 501 617,
  Result False (ldec (7.9625470000)) (udec (13.0529200000)) (ldec (1.2239819000)) (ldec (0.8556575900)) 611 615 635 639 491 613 509 619,
  Result False (ldec (7.9146460000)) (udec (12.9460400000)) (ldec (1.2156998000)) (ldec (0.8480077150)) 617 621 637 641 497 615 517 619,
  Result False (ldec (7.8516300000)) (udec (12.9460400000)) (ldec (1.2114343000)) (ldec (0.8459856400)) 623 627 637 641 507 617 525 621,
  Result False (ldec (7.7970140000)) (udec (12.8420800000)) (ldec (1.2065104500)) (ldec (0.8409553900)) 629 633 639 643 515 617 533 623,
  Result False (ldec (7.7330600000)) (udec (12.7745600000)) (ldec (1.1953546000)) (ldec (0.8339041100)) 635 639 641 645 523 619 541 625,
  Result False (ldec (7.6731500000)) (udec (12.7490700000)) (ldec (1.1862982500)) (ldec (0.8242569550)) 641 645 641 645 531 621 549 627,
  Result False (ldec (7.6179570000)) (udec (12.6573000000)) (ldec (1.1832791500)) (ldec (0.8238071300)) 647 651 643 647 539 623 557 627,
  Result False (ldec (7.5667980000)) (udec (12.6322700000)) (ldec (1.1837437000)) (ldec (0.8192699300)) 653 657 643 647 547 625 563 629,
  Result False (ldec (7.5147720000)) (udec (12.5420700000)) (ldec (1.1801413000)) (ldec (0.8154846550)) 659 663 645 649 555 627 573 631,
  Result False (ldec (7.4530300000)) (udec (12.5329500000)) (ldec (1.1667643500)) (ldec (0.8050450100)) 665 669 645 649 563 627 581 633,
  Result False (ldec (7.3955270000)) (udec (12.4398200000)) (ldec (1.1639827500)) (ldec (0.8047942100)) 671 675 647 651 571 629 589 633,
  Result False (ldec (7.3521150000)) (udec (12.4287000000)) (ldec (1.1595358000)) (ldec (0.8033539150)) 677 681 647 651 579 631 595 635,
  Result False (ldec (7.2845090000)) (udec (12.3300600000)) (ldec (1.1532078500)) (ldec (0.7919457450)) 683 687 649 653 587 633 603 637,
  Result False (ldec (7.2419510000)) (udec (12.3171500000)) (ldec (1.1475259000)) (ldec (0.7915428500)) 689 693 649 653 593 633 611 637,
  Result False (ldec (7.1720240000)) (udec (12.2331500000)) (ldec (1.1420387000)) (ldec (0.7869053300)) 695 699 651 655 601 635 619 639,
  Result False (ldec (7.1165010000)) (udec (12.2114200000)) (ldec (1.1378634500)) (ldec (0.7783875350)) 701 705 651 655 609 637 625 641,
  Result False (ldec (7.0542830000)) (udec (12.1165000000)) (ldec (1.1353706500)) (ldec (0.7717420950)) 707 711 653 657 617 637 635 643,
  Result False (ldec (7.0093640000)) (udec (12.0508800000)) (ldec (1.1308154000)) (ldec (0.7714024700)) 713 717 655 657 625 639 641 643,
  Result False (ldec (6.9535420000)) (udec (12.0093600000)) (ldec (1.1238576000)) (ldec (0.7677520950)) 719 723 655 659 633 641 649 645,
  Result False (ldec (6.9038390000)) (udec (11.9447700000)) (ldec (1.1207026500)) (ldec (0.7596086950)) 725 729 657 659 639 643 655 647,
  Result False (ldec (6.8450350000)) (udec (11.9038400000)) (ldec (1.1178479000)) (ldec (0.7592440850)) 731 735 657 661 647 643 663 647,
  Result False (ldec (6.7998730000)) (udec (11.8360800000)) (ldec (1.1153418000)) (ldec (0.7488777800)) 737 741 659 661 655 645 671 649,
  Result False (ldec (6.7383400000)) (udec (11.7997600000)) (ldec (1.1100968500)) (ldec (0.7435929300)) 743 747 659 663 663 647 679 651,
  Result False (ldec (6.6967820000)) (udec (11.7326600000)) (ldec (1.1066987000)) (ldec (0.7412417750)) 749 753 661 663 669 647 685 651,
  Result False (ldec (6.6329070000)) (udec (11.6892800000)) (ldec (1.1017283000)) (ldec (0.7364072250)) 755 759 661 665 677 649 693 653,
  Result False (ldec (6.5884130000)) (udec (11.6277600000)) (ldec (1.1014794000)) (ldec (0.7281779450)) 761 765 663 665 685 649 699 653,
  Result False (ldec (6.5444740000)) (udec (11.5879800000)) (ldec (1.0987985000)) (ldec (0.7263510000)) 767 771 663 665 691 651 707 655,
  Result False (ldec (6.4889670000)) (udec (11.5594800000)) (ldec (1.0907406000)) (ldec (0.7203922200)) 773 777 663 667 699 653 713 655,
  Result False (ldec (6.4330950000)) (udec (11.4739600000)) (ldec (1.0910664500)) (ldec (0.7187526150)) 779 783 665 667 707 655 721 657,
  Result False (ldec (6.3893630000)) (udec (11.4482900000)) (ldec (1.0866005000)) (ldec (0.7135550700)) 785 789 665 669 715 655 727 659,
  Result False (ldec (6.3372290000)) (udec (11.3708400000)) (ldec (1.0866176000)) (ldec (0.7065967950)) 791 795 667 669 721 657 735 659,
  Result False (ldec (6.2875390000)) (udec (11.3442000000)) (ldec (1.0790860000)) (ldec (0.7022793300)) 797 801 667 671 729 657 743 661,
  Result False (ldec (6.2411920000)) (udec (11.2745500000)) (ldec (1.0794185000)) (ldec (0.6988837450)) 803 807 669 671 737 659 749 661,
  Result False (ldec (6.1871590000)) (udec (11.2542300000)) (ldec (1.0750409000)) (ldec (0.6949614800)) 809 813 669 673 743 661 757 663,
  Result False (ldec (6.1388820000)) (udec (11.1720100000)) (ldec (1.0755330000)) (ldec (0.6918745500)) 815 819 671 673 751 661 763 665,
  Result False (ldec (6.0828490000)) (udec (11.1463700000)) (ldec (1.0687319500)) (ldec (0.6863982750)) 821 825 671 675 759 663 771 665,
  Result False (ldec (6.0382780000)) (udec (11.0728300000)) (ldec (1.0682740500)) (ldec (0.6770022050)) 827 831 673 675 765 663 777 667,
  Result False (ldec (5.9755950000)) (udec (11.0405200000)) (ldec (1.0647001500)) (ldec (0.6737842700)) 833 837 673 677 771 665 785 667,
  Result False (ldec (5.9404140000)) (udec (10.9728500000)) (ldec (1.0649661500)) (ldec (0.6665523950)) 839 843 675 677 779 665 793 669,
  Result False (ldec (5.8867400000)) (udec (10.9331500000)) (ldec (1.0603995000)) (ldec (0.6587542250)) 845 849 675 677 787 667 799 669,
  Result False (ldec (5.8406870000)) (udec (10.9074200000)) (ldec (1.0564437000)) (ldec (0.6562761500)) 851 855 675 679 793 667 807 671,
  Result False (ldec (5.7899060000)) (udec (10.8165400000)) (ldec (1.0568930500)) (ldec (0.6552012250)) 857 861 677 679 799 669 813 671,
  Result False (ldec (5.7390810000)) (udec (10.8027200000)) (ldec (1.0533714000)) (ldec (0.6517867350)) 863 867 677 681 807 671 821 673,
  Result False (ldec (5.6972540000)) (udec (10.7315200000)) (ldec (1.0516414500)) (ldec (0.6395934850)) 869 873 679 681 813 671 827 675,
  Result False (ldec (5.6434290000)) (udec (10.7052300000)) (ldec (1.0479649500)) (ldec (0.6375524100)) 875 879 679 683 821 673 835 675,
  Result False (ldec (5.5936310000)) (udec (10.6310500000)) (ldec (1.0480865500)) (ldec (0.6317502850)) 881 885 681 683 827 673 841 677,
  Result False (ldec (5.5503360000)) (udec (10.5936300000)) (ldec (1.0466216500)) (ldec (0.6287784950)) 887 891 681 683 835 675 849 677,
  Result False (ldec (5.5059920000)) (udec (10.5835400000)) (ldec (1.0409283000)) (ldec (0.6226318050)) 893 897 681 685 841 675 855 677,
  Result False (ldec (5.4610510000)) (udec (10.4890200000)) (ldec (1.0417852000)) (ldec (0.6200555000)) 899 903 683 685 849 677 861 679,
  Result False (ldec (5.4131390000)) (udec (10.4935800000)) (ldec (1.0378902000)) (ldec (0.6115002750)) 905 909 683 687 855 677 869 679,
  Result False (ldec (5.3715190000)) (udec (10.3989100000)) (ldec (1.0367521000)) (ldec (0.6071109900)) 911 915 685 687 863 679 875 681,
  Result False (ldec (4.8741950000)) (udec (10.8243000000)) (ldec (1.0271770500)) (ldec (0.6028631600)) 917 921 685 689 871 679 883 681,
  Result False (ldec (5.0695230000)) (udec (10.6793800000)) (ldec (1.0272454500)) (ldec (0.6001464450)) 923 927 685 689 877 681 889 683,
  Result False (ldec (4.5456390000)) (udec (10.9949800000)) (ldec (1.0210429000)) (ldec (0.5950090350)) 929 933 687 691 883 681 895 683,
  Result False (ldec (4.5456390000)) (udec (10.9949800000)) (ldec (1.0171175000)) (ldec (0.5914498600)) 935 939 687 691 889 683 903 685,
  Result False (ldec (5.1460830000)) (udec (10.1772200000)) (ldec (1.0279969000)) (ldec (0.5847319350)) 941 945 689 691 897 683 909 685,
  Result False (ldec (4.5547470000)) (udec (10.7300400000)) (ldec (1.0171716500)) (ldec (0.5797188800)) 947 951 689 693 903 685 917 687,
  Result False (ldec (4.5950000000)) (udec (10.7259300000)) (ldec (1.0157951000)) (ldec (0.5775893600)) 953 957 689 693 911 685 923 687,
  Result False (ldec (3.9183200000)) (udec (11.2084600000)) (ldec (1.0049679500)) (ldec (0.5742699650)) 959 963 691 695 917 687 931 689,
  Result False (ldec (3.9183200000)) (udec (11.2084600000)) (ldec (1.0034166000)) (ldec (0.5694956450)) 965 969 691 695 923 687 937 689,
  Result False (ldec (3.9092690000)) (udec (11.2063300000)) (ldec (1.0019811500)) (ldec (0.5617548550)) 971 975 691 695 931 689 943 691,
  Result False (ldec (3.6771220000)) (udec (11.2330700000)) (ldec (0.9984870500)) (ldec (0.5568760350)) 977 981 693 697 937 689 951 691,
  Result False (ldec (4.2032870000)) (udec (10.6644600000)) (ldec (1.0044293000)) (ldec (0.5540734400)) 983 987 693 697 943 689 957 693,
  Result False (ldec (4.7940160000)) (udec (9.8249400000)) (ldec (1.0152118000)) (ldec (0.5508322300)) 989 993 695 697 951 691 965 693,
  Result False (ldec (3.8194010000)) (udec (10.8274800000)) (ldec (0.9984861000)) (ldec (0.5403177250)) 995 999 695 699 957 691 971 695,
  Result False (ldec (4.7133500000)) (udec (9.7304200000)) (ldec (1.0118554500)) (ldec (0.5372757300)) 1001 1005 697 699 963 693 977 695,
  Result False (ldec (3.5822970000)) (udec (10.8505800000)) (ldec (0.9935537000)) (ldec (0.5342486500)) 1007 1011 697 701 971 693 985 695,
  Result False (ldec (3.5399910000)) (udec (10.8668300000)) (ldec (0.9916480000)) (ldec (0.5296330750)) 1013 1017 697 701 977 695 991 697,
  Result False (ldec (4.5634970000)) (udec (9.7417500000)) (ldec (1.0064167000)) (ldec (0.5230878600)) 1019 1023 699 701 983 695 997 697,
  Result False (ldec (3.1856050000)) (udec (11.0277900000)) (ldec (0.9852925000)) (ldec (0.5168812250)) 1025 1029 699 703 991 697 1005 699,
  Result False (ldec (3.1433050000)) (udec (11.0447900000)) (ldec (0.9832177000)) (ldec (0.5138032250)) 1031 1035 699 703 997 697 1011 699,
  Result False (ldec (3.1282970000)) (udec (10.9974900000)) (ldec (0.9834590000)) (ldec (0.5063838200)) 1037 1041 701 703 1003 697 1017 699,
  Result False (ldec (2.9101400000)) (udec (11.1179600000)) (ldec (0.9792172500)) (ldec (0.5020892500)) 1043 1047 701 705 1009 699 1023 701,
  Result False (ldec (2.9115180000)) (udec (11.1179600000)) (ldec (0.9781798500)) (ldec (0.4974874500)) 1049 1053 701 705 1017 699 1029 701,
  Result False (ldec (2.6414980000)) (udec (11.2095400000)) (ldec (0.9739447500)) (ldec (0.4955126850)) 1055 1059 703 707 1023 701 1037 703,
  Result False (ldec (2.5526350000)) (udec (11.2341900000)) (ldec (0.9719611500)) (ldec (0.4869473900)) 1061 1065 703 707 1031 701 1043 703,
  Result False (ldec (2.5776660000)) (udec (11.2341100000)) (ldec (0.9699832500)) (ldec (0.4817089950)) 1067 1071 703 707 1037 703 1049 703,
  Result False (ldec (2.2679570000)) (udec (11.3643800000)) (ldec (0.9670221000)) (ldec (0.4795298850)) 1073 1077 705 709 1045 703 1055 705,
  Result False (ldec (2.2687210000)) (udec (11.3537300000)) (ldec (0.9654897500)) (ldec (0.4710110450)) 1079 1083 705 709 1051 703 1063 705,
  Result False (ldec (3.5080410000)) (udec (10.0181300000)) (ldec (0.9834105500)) (ldec (0.4670919150)) 1085 1089 707 709 1057 705 1069 707,
  Result False (ldec (1.9119490000)) (udec (11.5073000000)) (ldec (0.9595798000)) (ldec (0.4626727050)) 1091 1095 707 711 1065 705 1075 707,
  Result False (ldec (1.8312100000)) (udec (11.5466000000)) (ldec (0.9584084500)) (ldec (0.4549033200)) 1097 1101 707 711 1071 705 1083 707,
  Result False (ldec (3.1712690000)) (udec (10.3866600000)) (ldec (0.9735723500)) (ldec (0.4505401600)) 1103 1107 709 711 1077 707 1089 709,
  Result False (ldec (1.5088630000)) (udec (11.6730500000)) (ldec (0.9530856000)) (ldec (0.4468921600)) 1109 1113 709 713 1083 707 1095 709,
  Result False (ldec (1.4677620000)) (udec (11.6850000000)) (ldec (0.9516644000)) (ldec (0.4373336400)) 1115 1119 709 713 1089 709 1101 709,
  Result False (ldec (1.5523770000)) (udec (11.5536100000)) (ldec (0.9529440500)) (ldec (0.4356680050)) 1121 1125 711 713 1097 709 1107 711,
  Result False (ldec (1.1944510000)) (udec (11.8254200000)) (ldec (0.9465180600)) (ldec (0.4265798300)) 1127 1131 711 715 1103 709 1115 711,
  Result False (ldec (1.1678680000)) (udec (11.8254200000)) (ldec (0.9450719700)) (ldec (0.4218097850)) 1133 1137 711 715 1109 711 1121 713,
  Result False (ldec (2.3444810000)) (udec (10.7889800000)) (ldec (0.9600614500)) (ldec (0.4192697700)) 1139 1143 713 715 1117 711 1127 713,
  Result False (ldec (0.7483290000)) (udec (12.0708200000)) (ldec (0.9399911800)) (ldec (0.4098467200)) 1145 1149 713 717 1123 713 1133 713,
  Result False (ldec (0.7055571000)) (udec (12.0925700000)) (ldec (0.9384905600)) (ldec (0.4068909850)) 1151 1155 713 717 1129 713 1141 715,
  Result False (ldec (2.0351440000)) (udec (10.9010100000)) (ldec (0.9534741500)) (ldec (0.3971529150)) 1157 1161 715 717 1135 713 1147 715,
  Result False (ldec (0.4257718000)) (udec (12.2286000000)) (ldec (0.9339670400)) (ldec (0.3944758150)) 1163 1167 715 719 1143 715 1153 715,
  Result False (ldec (0.3276367000)) (udec (12.2639400000)) (ldec (0.9314707250)) (ldec (0.3829223900)) 1169 1173 715 719 1149 715 1161 717,
  Result False (ldec (1.4123680000)) (udec (11.3751300000)) (ldec (0.9447138200)) (ldec (0.3792174850)) 1175 1179 717 719 1155 715 1167 717,
  Result False (ldec (-0.3001553000)) (udec (12.7376800000)) (ldec (0.9240262400)) (ldec (0.3730738350)) 1181 1185 717 721 1161 717 1173 717,
  Result False (ldec (-0.3001553000)) (udec (12.7376800000)) (ldec (0.9216185600)) (ldec (0.3716888300)) 1187 1191 717 721 1167 717 1179 719,
  Result False (ldec (-0.3653875000)) (udec (12.7585200000)) (ldec (0.9204393250)) (ldec (0.3707232500)) 1193 1197 717 721 1175 717 1187 719,
  Result False (ldec (-0.7230341000)) (udec (13.0336800000)) (ldec (0.9164599650)) (ldec (0.3594483650)) 1199 1203 719 721 1181 719 1193 719,
  Result False (ldec (0.7835814000)) (udec (11.1760100000)) (ldec (0.9393747250)) (ldec (0.3565900050)) 1205 1209 719 723 1187 719 1199 721,
  Result False (ldec (2.2667540000)) (udec (9.7798100000)) (ldec (0.9580626500)) (ldec (0.3511350100)) 1211 1215 721 723 1193 719 1205 721,
  Result False (ldec (0.8091586000)) (udec (11.0242500000)) (ldec (0.9397846500)) (ldec (0.3477752400)) 1217 1221 721 723 1201 721 1211 721,
  Result False (ldec (0.1987889000)) (udec (11.5489600000)) (ldec (0.9307584150)) (ldec (0.3418425850)) 1223 1227 721 725 1207 721 1217 723,
  Result False (ldec (0.3138537000)) (udec (11.4164200000)) (ldec (0.9320484200)) (ldec (0.3218987600)) 1229 1233 723 725 1213 721 1223 723,
  Result False (ldec (0.5138526000)) (udec (11.6177100000)) (ldec (0.9293205900)) (ldec (0.3155732800)) 1235 1239 723 725 1219 723 1231 723,
  Result False (ldec (-1.5009600000)) (udec (13.2845100000)) (ldec (0.9025841700)) (ldec (0.3122257650)) 1241 1245 723 727 1225 723 1237 725,
  Result False (ldec (-1.5009600000)) (udec (13.2845100000)) (ldec (0.9025614650)) (ldec (0.3103471400)) 1247 1251 723 727 1231 723 1243 725,
  Result False (ldec (0.0000000000)) (udec (10.0000000000)) (ldec (0.9437921300)) (ldec (0.3097961400)) 1253 1257 725 727 1239 725 1249 725,
  Result False (ldec (1.3288970000)) (udec (9.9700100000)) (ldec (0.9458162000)) (ldec (0.3097961400)) 1259 1263 725 727 1245 725 1257 727,
  Result False (ldec (2.5354330000)) (udec (8.4873500000)) (ldec (0.9643231500)) (ldec (0.3098531400)) 1265 1269 727 727 1251 725 1259 727
]"

end