sat ((f0m false) (f0c 591426) (f1m false) (f1c 356954) (f2m false) (f2c 815405) (f3m true) (f3c 2096187) (f4m true) (f4c 2099646) (f5m true) (f5c 587906) (f6m true) (f6c 139972) (f7m true) (f7c (- 108528)) (f8m true) (f8c 363942) (f9m true) (f9c 2218695) (f10m true) (f10c 1980719) (f11m true) (f11c 1984210) (f12m false) (f12c 822427) (f13m false) (f13c 580946) (f14m false) (f14c 1063835) (f15m false) (f15c 1056903) (f16m false) (f16c 822433) (f17m false) (f17c 1298306) (f18m false) (f18c 598451) (f19m false) (f19c 122456) (f20m false) (f20c 822424) (f21m true) (f21c 465394) (f22m true) (f22c 2092736) (f23m false) (f23c 241417) (f24m false) (f24c 293842) (f25m false) (f25c 52352) (f26m true) (f26c 475852) (f27m true) (f27c 1) (f28m true) (f28c (- 234482)) (f29m true) (f29c 237943) (f30m true) (f30c 10408) (f31m true) (f31c (- 234480)) (f32m true) (f32c 241392) (f33m true) (f33c 1039250) (f34m true) (f34c 752404) (f35m true) (f35c 1984210) (f36m false) (f36c 549417) (f37m false) (f37c 304541) (f38m true) (f38c 780411) (f39m false) (f39c 783897) (f40m false) (f40c 475883) (f41m false) (f41c 1021891) (f42m false) (f42c 318432) (f43m false) (f43c 73549) (f44m false) (f44c 549422) (f45m false) (f45c 195979) (f46m false) (f46c 440866) (f47m false) (f47c (- 35006)) (f48m false) (f48c 0) (f49m true) (f49c (- 237935)) (f50m true) (f50c 2215223) (f51m true) (f51c (- 237979)) (f52m true) (f52c 1504768) (f53m true) (f53c 0) (f54m true) (f54c (- 234484)) (f55m true) (f55c (- 472420)) (f56m true) (f56c 0) (f57m true) (f57c 2218695) (f58m true) (f58c 1980718) (f59m true) (f59c 1984210) (f60m false) (f60c 353463) (f61m false) (f61c 122447) (f62m false) (f62c 587914) (f63m false) (f63c 591422) (f64m false) (f64c 356935) (f65m false) (f65c 433923) (f66m false) (f66c 139970) (f67m true) (f67c (- 108530)) (f68m true) (f68c 363940) (f69m true) (f69c (- 14)) (f70m true) (f70c 237952) (f71m false) (f71c (- 234467)) (f72m true) (f72c 119002) (f73m false) (f73c (- 115488)) (f74m true) (f74c 335962) (f75m true) (f75c (- 112029)) (f76m true) (f76c (- 329025)) (f77m true) (f77c 122424) (f78m true) (f78c (- 111979)) (f79m true) (f79c (- 339461)) (f80m true) (f80c 111993) (f81m false) (f81c 83970) (f82m true) (f82c 1980721) (f83m true) (f83c 241468) (f84m false) (f84c 237963) (f85m true) (f85c 1) (f86m true) (f86c 475919) (f87m false) (f87c 472429) (f88m false) (f88c 237941) (f89m true) (f89c 710411) (f90m true) (f90c 0) (f91m false) (f91c (- 234483)) (f92m false) (f92c 237942) (f93m true) (f93c (- 35014)) (f94m true) (f94c 199459) (f95m true) (f95c (- 272968)) (f96m true) (f96c (- 1448768)) (f97m true) (f97c (- 1683237)) (f98m true) (f98c (- 1217774)) (f99m true) (f99c (- 1214328)) (f100m true) (f100c (- 1448754)) (f101m true) (f101c 864477) (f102m true) (f102c (- 1686753)) (f103m true) (f103c (- 1921224)) (f104m true) (f104c (- 1455761)) (f105m false) (f105c 0) (f106m false) (f106c 248500) (f107m true) (f107c 171512) (f108m false) (f108c 1413857) (f109m false) (f109c 1179387) (f110m false) (f110c 1655261) (f111m true) (f111c 2918615) (f112m true) (f112c 2922080) (f113m true) (f113c 3397953) (f114m true) (f114c 1109248) (f115m true) (f115c 864368) (f116m true) (f116c 1340238) (f117m false) (f117c 1056822) (f118m true) (f118c 4192383) (f119m true) (f119c 1984209) (f120m false) (f120c 1056822) (f121m true) (f121c 4192384) (f122m true) (f122c 1984210) (f123m false) (f123c 1098834) (f124m false) (f124c 853958) (f125m false) (f125c 1326432) (f126m false) (f126c 1340323) (f127m false) (f127c 1095440) (f128m false) (f128c 1571313) (f129m false) (f129c 867854) (f130m false) (f130c 622973) (f131m false) (f131c 1098844) (f132m false) (f132c 745407) (f133m false) (f133c 986885) (f134m false) (f134c 514416) (f135m false) (f135c 745407) (f136m false) (f136c 986885) (f137m false) (f137c 514416) (f138m false) (f138c 1392676) (f139m false) (f139c 1147800) (f140m false) (f140c 1623665) (f141m true) (f141c 1175918) (f142m true) (f142c 860959) (f143m true) (f143c 3397950) (f144m true) (f144c 1109247) (f145m true) (f145c 864367) (f146m true) (f146c 1340237) (f147m false) (f147c 1039249) (f148m true) (f148c 752404) (f149m true) (f149c 755815) (f150m false) (f150c 1039249) (f151m true) (f151c 752405) (f152m true) (f152c 1984210) (f153m false) (f153c 353463) (f154m false) (f154c 122447) (f155m false) (f155c 587914) (f156m true) (f156c 2096188) (f157m true) (f157c (- 108532)) (f158m true) (f158c 1938691) (f159m true) (f159c 139971) (f160m true) (f160c (- 108529)) (f161m true) (f161c 363941) (f162m true) (f162c 1980758) (f163m true) (f163c 1980720) (f164m true) (f164c (- 234467)) (f165m true) (f165c 2218694) (f166m true) (f166c 1980719) (f167m true) (f167c (- 234466)) (f168m false) (f168c 843259) (f169m false) (f169c 598383) (f170m false) (f170c 1074243) (f171m true) (f171c 713950) (f172m true) (f172c 384842) (f173m true) (f173c 948402) (f174m true) (f174c 608894) (f175m true) (f175c 374413) (f176m true) (f176c 829400) (f177m false) (f177c 493218) (f178m true) (f178c 206385) (f179m true) (f179c 206387) (f180m false) (f180c 493218) (f181m true) (f181c 1980723) (f182m true) (f182c 1984256) (f183m false) (f183c 727884) (f184m false) (f184c 479382) (f185m false) (f185c 941377) (f186m false) (f186c 948357) (f187m false) (f187c 713870) (f188m false) (f188c 1179336) (f189m false) (f189c 493433) (f190m false) (f190c 262417) (f191m false) (f191c 727884) (f192m false) (f192c 353447) (f193m false) (f193c 199456) (f194m true) (f194c 129426) (f195m false) (f195c 353447) (f196m false) (f196c 199456) (f197m false) (f197c (- 234467)) (f198m false) (f198c 832869) (f199m false) (f199c 598382) (f200m false) (f200c 1063848) (f201m true) (f201c 615857) (f202m true) (f202c 384841) (f203m true) (f203c 850308) (f204m true) (f204c 608893) (f205m true) (f205c 374411) (f206m true) (f206c 829399) (f207m false) (f207c 83968) (f208m true) (f208c 1882628) (f209m true) (f209c 241468) (f210m false) (f210c 83970) (f211m true) (f211c 1980722) (f212m true) (f212c 241469) (f213m false) (f213c 475934) (f214m false) (f214c 241447) (f215m false) (f215c 318435) (f216m true) (f216c 262394) (f217m true) (f217c 27911) (f218m true) (f218c 475885) (f219m true) (f219c 251962) (f220m true) (f220c 10468) (f221m true) (f221c 475935) (f222m true) (f222c 101493) (f223m true) (f223c (- 112043)) (f224m true) (f224c (- 111993)) (f225m false) (f225c 83970) (f226m true) (f226c 1980720) (f227m true) (f227c 1984211) (f228m false) (f228c 475926) (f229m true) (f229c 241436) (f230m true) (f230c 713853) (f231m false) (f231c 710392) (f232m false) (f232c 475882) (f233m true) (f233c 948353) (f234m false) (f234c 237946) (f235m false) (f235c 3459) (f236m false) (f236c 475884) (f237m true) (f237c 202949) (f238m true) (f238c 437443) (f239m true) (f239c (- 2131258)) (f240m true) (f240c (- 35013)) (f241m true) (f241c 475951) (f242m true) (f242c (- 2131257)) (f243m false) (f243c 475926) (f244m true) (f244c 241438) (f245m true) (f245c 713851) (f246m true) (f246c 237946) (f247m true) (f247c 3459) (f248m true) (f248c 475884) (f249m true) (f249c 251961) (f250m true) (f250c 6951) (f251m true) (f251c 475934) (f252m true) (f252c 83968) (f253m true) (f253c 1980719) (f254m true) (f254c 3532) (f255m true) (f255c 83969) (f256m true) (f256c 1980719) (f257m true) (f257c 1984210) (f258m false) (f258c 237963) (f259m true) (f259c 52349) (f260m true) (f260c 475852) (f261m true) (f261c 0) (f262m true) (f262c (- 234483)) (f263m true) (f263c 237942) (f264m true) (f264c 10407) (f265m true) (f265c (- 234481)) (f266m true) (f266c 237992) (f267m true) (f267c 1039248) (f268m true) (f268c (- 272969)) (f269m true) (f269c (- 269501)) (f270m true) (f270c 1039249) (f271m true) (f271c (- 272968)) (f272m true) (f272c 1984210) (f273m false) (f273c 591426) (f274m false) (f274c 360410) (f275m false) (f275c 825877) (f276m false) (f276c 829363) (f277m false) (f277c 594876) (f278m false) (f278c 1060343) (f279m false) (f279c 377912) (f280m false) (f280c 122452) (f281m false) (f281c 199440) (f282m true) (f282c 241454) (f283m true) (f283c 475946) (f284m false) (f284c 3475) (f285m true) (f285c 2218694) (f286m true) (f286c 475947) (f287m false) (f287c 3475) (f288m false) (f288c 591426) (f289m false) (f289c 360410) (f290m false) (f290c 825877) (f291m true) (f291c 377914) (f292m true) (f292c 2099645) (f293m true) (f293c 587905) (f294m true) (f294c 377913) (f295m true) (f295c 125927) (f296m true) (f296c 591394) (f297m true) (f297c 2218696) (f298m true) (f298c 1980716) (f299m true) (f299c 1984210) (f300m true) (f300c 2218696) (f301m true) (f301c 1980717) (f302m true) (f302c 1984210) (f303m false) (f303c 1662286) (f304m false) (f304c 1403379) (f305m false) (f305c 1886262) (f306m false) (f306c 1896757) (f307m false) (f307c 1644866) (f308m false) (f308c 2120739) (f309m false) (f309c 1420878) (f310m false) (f310c 1179397) (f311m false) (f311c 1662286) (f312m false) (f312c 1305252) (f313m false) (f313c 1539723) (f314m false) (f314c 1063841) (f315m false) (f315c 1305252) (f316m false) (f316c 1539723) (f317m false) (f317c 1063841) (f318m false) (f318c 1098834) (f319m false) (f319c 853958) (f320m false) (f320c 1326432) (f321m false) (f321c 1340323) (f322m false) (f322c 1095440) (f323m false) (f323c 1571313) (f324m false) (f324c 867854) (f325m false) (f325c 622973) (f326m false) (f326c 1098844) (f327m false) (f327c 745407) (f328m false) (f328c 986885) (f329m false) (f329c 514416) (f330m false) (f330c 745407) (f331m false) (f331c 986885) (f332m false) (f332c 514416) (f333m false) (f333c 1648251) (f334m false) (f334c 1403375) (f335m false) (f335c 1875854) (f336m false) (f336c 1889745) (f337m false) (f337c 1644864) (f338m false) (f338c 2120735) (f339m false) (f339c 1417276) (f340m false) (f340c 1172395) (f341m false) (f341c 1648266) (f342m false) (f342c 1294824) (f343m false) (f343c 1536307) (f344m false) (f344c 1063839) (f345m false) (f345c 1294824) (f346m false) (f346c 1536307) (f347m false) (f347c 1063839) (f348m false) (f348c 591426) (f349m false) (f349c 360410) (f350m false) (f350c 825877) (f351m false) (f351c 829363) (f352m false) (f352c 594876) (f353m false) (f353c 1060343) (f354m false) (f354c 377912) (f355m false) (f355c 122452) (f356m false) (f356c 199440) (f357m true) (f357c 237951) (f358m true) (f358c 475893) (f359m false) (f359c 3475) (f360m true) (f360c 465395) (f361m true) (f361c 199459) (f362m false) (f362c 3475) (f363m false) (f363c 1098834) (f364m false) (f364c 853958) (f365m false) (f365c 1326432) (f366m false) (f366c 1340323) (f367m false) (f367c 1095440) (f368m false) (f368c 1571313) (f369m false) (f369c 867854) (f370m false) (f370c 622973) (f371m false) (f371c 1098844) (f372m false) (f372c 745407) (f373m false) (f373c 986885) (f374m false) (f374c 514416) (f375m false) (f375c 745407) (f376m false) (f376c 986885) (f377m false) (f377c 514416) (f378m false) (f378c 727884) (f379m false) (f379c 479382) (f380m false) (f380c 941377) (f381m false) (f381c 948357) (f382m false) (f382c 713870) (f383m false) (f383c 1179336) (f384m false) (f384c 493433) (f385m false) (f385c 262417) (f386m false) (f386c 727884) (f387m false) (f387c 353447) (f388m false) (f388c 199456) (f389m true) (f389c 129422) (f390m false) (f390c 353447) (f391m false) (f391c 199456) (f392m false) (f392c (- 234467)) (f393m false) (f393c 1081347) (f394m false) (f394c 850331) (f395m false) (f395c 1315798) (f396m false) (f396c 1319306) (f397m false) (f397c 1070805) (f398m false) (f398c 1536271) (f399m false) (f399c 867854) (f400m false) (f400c 619352) (f401m false) (f401c 1081347) (f402m false) (f402c 706910) (f403m false) (f403c 944869) (f404m false) (f404c 493417) (f405m false) (f405c 706910) (f406m false) (f406c 944869) (f407m false) (f407c 493417) (f408m false) (f408c 727884) (f409m false) (f409c 479382) (f410m false) (f410c 941377) (f411m false) (f411c 948357) (f412m false) (f412c 713870) (f413m false) (f413c 1179336) (f414m false) (f414c 493433) (f415m false) (f415c 262417) (f416m false) (f416c 727884) (f417m false) (f417c 353447) (f418m false) (f418c 199456) (f419m true) (f419c 129473) (f420m false) (f420c 353447) (f421m false) (f421c 199456) (f422m false) (f422c (- 234467)) (f423m false) (f423c 475926) (f424m true) (f424c 241401) (f425m true) (f425c 710392) (f426m false) (f426c 710392) (f427m false) (f427c 475882) (f428m true) (f428c 948352) (f429m false) (f429c 237946) (f430m false) (f430c 3459) (f431m false) (f431c 475884) (f432m true) (f432c 202951) (f433m true) (f433c 437443) (f434m true) (f434c (- 35024)) (f435m true) (f435c 202952) (f436m true) (f436c 199459) (f437m true) (f437c (- 35025)) (f438m false) (f438c 713889) (f439m true) (f439c 479383) (f440m true) (f440c 948353) (f441m false) (f441c 948355) (f442m false) (f442c 713823) (f443m true) (f443c 1186297) (f444m false) (f444c 475909) (f445m false) (f445c 241401) (f446m false) (f446c 713826) (f447m true) (f447c 440915) (f448m true) (f448c 675383) (f449m true) (f449c (- 35024)) (f450m true) (f450c 440915) (f451m true) (f451c 199458) (f452m true) (f452c (- 272967)) (f453m true) (f453c (- 1210804)) (f454m true) (f454c (- 1445305)) (f455m true) (f455c 864480) (f456m true) (f456c (- 976342)) (f457m true) (f457c (- 1210813)) (f458m true) (f458c 1102418) (f459m true) (f459c (- 1448811)) (f460m true) (f460c (- 1683237)) (f461m true) (f461c 629994) (f462m false) (f462c 237963) (f463m false) (f463c 486441) (f464m false) (f464c 14017) (f465m false) (f465c 237963) (f466m false) (f466c 486441) (f467m false) (f467c 14017) (f468m false) (f468c 1371844) (f469m false) (f469c 1130363) (f470m false) (f470c 1613252) (f471m false) (f471c 1620342) (f472m false) (f472c 1364843) (f473m false) (f473c 1847732) (f474m false) (f474c 1147873) (f475m false) (f475c 899378) (f476m false) (f476c 1382267) (f477m true) (f477c 1021828) (f478m false) (f478c 1263308) (f479m false) (f479c 790839) (f480m false) (f480c 195979) (f481m false) (f481c 1263308) (f482m false) (f482c 790839) (f483m false) (f483c 1742789) (f484m false) (f484c 1487292) (f485m false) (f485c 1970181) (f486m false) (f486c 1977277) (f487m false) (f487c 1721785) (f488m false) (f488c 2204674) (f489m false) (f489c 1511814) (f490m false) (f490c 1270333) (f491m false) (f491c 1753222) (f492m false) (f492c 1385755) (f493m false) (f493c 1620243) (f494m false) (f494c 335949) (f495m false) (f495c 1385755) (f496m false) (f496c 1620243) (f497m false) (f497c 335949) (f498m false) (f498c 1980752) (f499m false) (f499c 1725255) (f500m false) (f500c 2208144) (f501m false) (f501c 2215218) (f502m false) (f502c 1959726) (f503m false) (f503c 2442615) (f504m false) (f504c 1749756) (f505m false) (f505c 1508275) (f506m false) (f506c 1991164) (f507m false) (f507c 1623718) (f508m false) (f508c 1858184) (f509m false) (f509c 1385760) (f510m false) (f510c 1623718) (f511m false) (f511c 1858184) (f512m false) (f512c 1385760) (f513m true) (f513c 531982) (f514m true) (f514c 290501) (f515m true) (f515c 759376) (f516m true) (f516c 2614233) (f517m true) (f517c 2372752) (f518m true) (f518c 993861) (f519m true) (f519c 293999) (f520m true) (f520c 38502) (f521m true) (f521c 521391) (f522m true) (f522c 167986) (f523m true) (f523c 2250237) (f524m true) (f524c (- 63035)) (f525m false) (f525c 0) (f526m false) (f526c 248500) (f527m true) (f527c 171512) (f528m false) (f528c 475926) (f529m true) (f529c 237965) (f530m true) (f530c 780413) (f531m false) (f531c 710392) (f532m false) (f532c 475882) (f533m true) (f533c 1021893) (f534m false) (f534c 237946) (f535m false) (f535c 3459) (f536m false) (f536c 475884) (f537m true) (f537c 202951) (f538m true) (f538c 199459) (f539m true) (f539c (- 35024)) (f540m true) (f540c 202951) (f541m true) (f541c 199459) (f542m true) (f542c (- 35023)) (f543m true) (f543c (- 1098840)) (f544m true) (f544c (- 1333310)) (f545m true) (f545c (- 867847)) (f546m true) (f546c 2845195) (f547m true) (f547c 752544) (f548m true) (f548c 3076185) (f549m true) (f549c 524950) (f550m true) (f550c (- 1557284)) (f551m true) (f551c 755947) (f552m false) (f552c 370947) (f553m false) (f553c 605435) (f554m false) (f554c 139970) (f555m false) (f555c 370947) (f556m false) (f556c 605435) (f557m false) (f557c 139970) (f558m false) (f558c 1382267) (f559m false) (f559c 1137384) (f560m false) (f560c 1613257) (f561m false) (f561c 1616738) (f562m false) (f562c 1371855) (f563m false) (f563c 1847728) (f564m false) (f564c 1147868) (f565m false) (f565c 902992) (f566m false) (f566c 1371846) (f567m false) (f567c 1028829) (f568m false) (f568c 1263300) (f569m false) (f569c 794430) (f570m false) (f570c 1028829) (f571m false) (f571c 1263300) (f572m false) (f572c 794430) (f573m false) (f573c 2211703) (f574m false) (f574c 1966827) (f575m false) (f575c 2435684) (f576m false) (f576c 2446174) (f577m false) (f577c 2201298) (f578m false) (f578c 2670161) (f579m false) (f579c 1980718) (f580m false) (f580c 1735835) (f581m false) (f581c 2211708) (f582m false) (f582c 1858265) (f583m false) (f583c 2092736) (f584m false) (f584c 1627280) (f585m false) (f585c 1858265) (f586m false) (f586c 2092736) (f587m false) (f587c 1627280) (f588m true) (f588c (- 1098840)) (f589m true) (f589c 518061) (f590m true) (f590c (- 867847)) (f591m true) (f591c 2845195) (f592m true) (f592c 752544) (f593m true) (f593c 3076185) (f594m true) (f594c 524950) (f595m true) (f595c 280074) (f596m true) (f596c 755947) (f597m true) (f597c 0) (f598m true) (f598c 2491757) (f599m true) (f599c 171512) (f600m false) (f600c 0) (f601m false) (f601c 248500) (f602m true) (f602c 171512) (f603m false) (f603c 591426) (f604m false) (f604c 360410) (f605m false) (f605c 825877) (f606m false) (f606c 829363) (f607m false) (f607c 594876) (f608m false) (f608c 1060343) (f609m false) (f609c 377912) (f610m false) (f610c 122452) (f611m false) (f611c 199440) (f612m true) (f612c 237949) (f613m true) (f613c 472413) (f614m false) (f614c 3475) (f615m true) (f615c (- 35015)) (f616m true) (f616c 199469) (f617m false) (f617c 3475) (f618m false) (f618c 829389) (f619m false) (f619c 598373) (f620m false) (f620c 1063840) (f621m false) (f621c 1067304) (f622m false) (f622c 832839) (f623m false) (f623c 1298306) (f624m false) (f624c 615854) (f625m false) (f625c 360394) (f626m false) (f626c 825860) (f627m true) (f627c 202946) (f628m true) (f628c 437412) (f629m false) (f629c 241417) (f630m true) (f630c 202945) (f631m true) (f631c 199458) (f632m false) (f632c 241417))