sat ((f0m false) (f0c 118) (f1m true) (f1c 0) (f2m true) (f2c 218) (f3m true) (f3c 0) (f4m true) (f4c 782) (f5m true) (f5c 881) (f6m true) (f6c (- 88)) (f7m true) (f7c (- 392)) (f8m false) (f8c 220) (f9m true) (f9c (- 266)) (f10m false) (f10c 663) (f11m true) (f11c 882) (f12m true) (f12c 111) (f13m true) (f13c (- 347)) (f14m false) (f14c 1004) (f15m true) (f15c 119) (f16m false) (f16c 661) (f17m true) (f17c 1005) (f18m true) (f18c 8) (f19m false) (f19c (- 883)) (f20m false) (f20c 883) (f21m true) (f21c (- 18)) (f22m false) (f22c 0) (f23m false) (f23c 882) (f24m false) (f24c (- 1)) (f25m false) (f25c (- 1695)) (f26m true) (f26c 710) (f27m true) (f27c (- 666)) (f28m false) (f28c 0) (f29m true) (f29c 881) (f30m false) (f30c 21) (f31m false) (f31c (- 982)) (f32m true) (f32c 721) (f33m true) (f33c 21) (f34m true) (f34c 696) (f35m true) (f35c 1421) (f36m true) (f36c (- 939)) (f37m true) (f37c (- 482)) (f38m true) (f38c (- 44)) (f39m true) (f39c (- 532)) (f40m true) (f40c 663) (f41m false) (f41c 883) (f42m false) (f42c 663) (f43m false) (f43c 883) (f44m true) (f44c (- 393)) (f45m true) (f45c (- 877)) (f46m true) (f46c 77) (f47m true) (f47c (- 415)) (f48m true) (f48c 661) (f49m false) (f49c 1667) (f50m false) (f50c 661) (f51m false) (f51c 1667) (f52m true) (f52c (- 284)) (f53m true) (f53c (- 764)) (f54m true) (f54c 198) (f55m true) (f55c (- 296)) (f56m true) (f56c 772) (f57m false) (f57c 1665) (f58m false) (f58c 661) (f59m false) (f59c 1665) (f60m true) (f60c (- 177)) (f61m true) (f61c (- 852)) (f62m true) (f62c (- 66)) (f63m true) (f63c (- 562)) (f64m true) (f64c 1273) (f65m false) (f65c 881) (f66m false) (f66c 663) (f67m false) (f67c 881) (f68m true) (f68c (- 64)) (f69m true) (f69c (- 562)) (f70m true) (f70c 41) (f71m true) (f71c (- 634)) (f72m false) (f72c 781) (f73m true) (f73c 882) (f74m false) (f74c 781) (f75m true) (f75c 881) (f76m false) (f76c 0) (f77m true) (f77c (- 885)) (f78m true) (f78c 889) (f79m false) (f79c 0) (f80m false) (f80c (- 1)) (f81m false) (f81c 883) (f82m false) (f82c 0) (f83m false) (f83c 883) (f84m true) (f84c (- 370)) (f85m true) (f85c (- 893)) (f86m false) (f86c 1004) (f87m true) (f87c 119) (f88m true) (f88c 536) (f89m false) (f89c 1004) (f90m false) (f90c 661) (f91m false) (f91c 1004) (f92m true) (f92c (- 261)) (f93m true) (f93c (- 782)) (f94m true) (f94c 213) (f95m true) (f95c 238) (f96m true) (f96c 661) (f97m false) (f97c 1665) (f98m false) (f98c 661) (f99m false) (f99c 1665) (f100m true) (f100c (- 179)) (f101m true) (f101c (- 854)) (f102m true) (f102c (- 61)) (f103m true) (f103c (- 562)) (f104m true) (f104c 573) (f105m false) (f105c 881) (f106m false) (f106c 663) (f107m false) (f107c 881) (f108m true) (f108c (- 63)) (f109m true) (f109c (- 562)) (f110m true) (f110c 40) (f111m true) (f111c (- 635)) (f112m false) (f112c 781) (f113m true) (f113c 882) (f114m false) (f114c 781) (f115m true) (f115c 883) (f116m true) (f116c (- 172)) (f117m true) (f117c (- 800)) (f118m true) (f118c (- 46)) (f119m true) (f119c (- 496)) (f120m true) (f120c 663) (f121m false) (f121c 883) (f122m false) (f122c 663) (f123m false) (f123c 883) (f124m true) (f124c (- 798)) (f125m true) (f125c (- 888)) (f126m true) (f126c (- 312)) (f127m true) (f127c (- 758)) (f128m true) (f128c 663) (f129m false) (f129c 883) (f130m false) (f130c 663) (f131m false) (f131c 883) (f132m true) (f132c (- 886)) (f133m true) (f133c (- 978)) (f134m true) (f134c (- 578)) (f135m true) (f135c (- 488)) (f136m true) (f136c 663) (f137m false) (f137c 883) (f138m false) (f138c 663) (f139m false) (f139c 883) (f140m true) (f140c (- 974)) (f141m true) (f141c (- 878)) (f142m true) (f142c (- 844)) (f143m true) (f143c (- 756)) (f144m true) (f144c 663) (f145m false) (f145c 883) (f146m false) (f146c 663) (f147m false) (f147c 883) (f148m true) (f148c (- 856)) (f149m true) (f149c (- 758)) (f150m true) (f150c 589) (f151m true) (f151c (- 659)) (f152m false) (f152c 781) (f153m true) (f153c 883) (f154m false) (f154c 781) (f155m true) (f155c 881) (f156m false) (f156c 42) (f157m false) (f157c (- 961)) (f158m true) (f158c 165) (f159m true) (f159c (- 881)) (f160m true) (f160c 694) (f161m true) (f161c 1419) (f162m true) (f162c 695) (f163m true) (f163c 1420) (f164m true) (f164c (- 225)) (f165m true) (f165c (- 1275)) (f166m false) (f166c 262) (f167m false) (f167c (- 741)) (f168m true) (f168c 1029) (f169m true) (f169c 1152) (f170m false) (f170c 663) (f171m true) (f171c 1151) (f172m true) (f172c (- 130)) (f173m true) (f173c (- 1896)) (f174m true) (f174c (- 4)) (f175m true) (f175c (- 1005)) (f176m true) (f176c 573) (f177m false) (f177c 883) (f178m false) (f178c 663) (f179m false) (f179c 883) (f180m true) (f180c (- 122)) (f181m true) (f181c (- 1888)) (f182m true) (f182c (- 22)) (f183m true) (f183c (- 1019)) (f184m false) (f184c 0) (f185m false) (f185c 1546) (f186m false) (f186c 0) (f187m false) (f187c 1546) (f188m true) (f188c (- 1717)) (f189m true) (f189c (- 2716)) (f190m true) (f190c 588) (f191m true) (f191c (- 1178)) (f192m false) (f192c (- 1)) (f193m true) (f193c 710) (f194m false) (f194c 0) (f195m true) (f195c 881) (f196m true) (f196c 220) (f197m true) (f197c (- 236)) (f198m true) (f198c 1119) (f199m true) (f199c 238) (f200m true) (f200c 660) (f201m false) (f201c 1665) (f202m false) (f202c 661) (f203m false) (f203c 1665) (f204m true) (f204c 226) (f205m true) (f205c (- 228)) (f206m true) (f206c 1103) (f207m true) (f207c 220) (f208m false) (f208c 782) (f209m false) (f209c 1544) (f210m false) (f210c 782) (f211m false) (f211c 1544) (f212m true) (f212c 223) (f213m true) (f213c (- 229)) (f214m true) (f214c 936) (f215m true) (f215c 482) (f216m false) (f216c 781) (f217m true) (f217c 880) (f218m false) (f218c 781) (f219m true) (f219c 881) (f220m true) (f220c 222) (f221m true) (f221c (- 229)) (f222m true) (f222c 935) (f223m true) (f223c (- 174)) (f224m false) (f224c 781) (f225m true) (f225c 880) (f226m false) (f226c 781) (f227m true) (f227c 881) (f228m true) (f228c 224) (f229m true) (f229c (- 228)) (f230m true) (f230c 1127) (f231m true) (f231c 238) (f232m true) (f232c 774) (f233m false) (f233c 1665) (f234m false) (f234c 661) (f235m false) (f235c 1665) (f236m true) (f236c 244) (f237m true) (f237c (- 645)) (f238m true) (f238c 1107) (f239m true) (f239c 655) (f240m false) (f240c 782) (f241m false) (f241c 1544) (f242m false) (f242c 782) (f243m false) (f243c 1544) (f244m true) (f244c 245) (f245m true) (f245c (- 803)) (f246m true) (f246c 954) (f247m true) (f247c 65) (f248m false) (f248c 781) (f249m true) (f249c 881) (f250m false) (f250c 781) (f251m true) (f251c 881) (f252m true) (f252c 220) (f253m true) (f253c (- 236)) (f254m true) (f254c 339) (f255m true) (f255c 238) (f256m true) (f256c 772) (f257m false) (f257c 1665) (f258m false) (f258c 661) (f259m false) (f259c 1665) (f260m true) (f260c 130) (f261m true) (f261c (- 154)) (f262m true) (f262c 440) (f263m true) (f263c (- 28)) (f264m true) (f264c 573) (f265m false) (f265c 881) (f266m false) (f266c 663) (f267m false) (f267c 881) (f268m true) (f268c 246) (f269m true) (f269c (- 36)) (f270m true) (f270c 348) (f271m true) (f271c 64) (f272m false) (f272c 781) (f273m true) (f273c 881) (f274m false) (f274c 781) (f275m true) (f275c 881) (f276m true) (f276c 346) (f277m true) (f277c (- 1425)) (f278m true) (f278c 1231) (f279m true) (f279c (- 532)) (f280m true) (f280c 663) (f281m false) (f281c 883) (f282m false) (f282c 663) (f283m false) (f283c 883) (f284m true) (f284c 884) (f285m true) (f285c (- 879)) (f286m true) (f286c 1350) (f287m true) (f287c (- 421)) (f288m true) (f288c 661) (f289m false) (f289c 1667) (f290m false) (f290c 661) (f291m false) (f291c 1667) (f292m true) (f292c 983) (f293m true) (f293c (- 768)) (f294m true) (f294c 1469) (f295m true) (f295c (- 302)) (f296m true) (f296c 661) (f297m false) (f297c 1665) (f298m false) (f298c 661) (f299m false) (f299c 1665) (f300m true) (f300c 1077) (f301m true) (f301c (- 694)) (f302m true) (f302c 1203) (f303m true) (f303c (- 568)) (f304m true) (f304c 663) (f305m false) (f305c 881) (f306m false) (f306c 663) (f307m false) (f307c 881) (f308m true) (f308c 990) (f309m true) (f309c (- 960)) (f310m true) (f310c 937) (f311m true) (f311c (- 100)) (f312m true) (f312c 489) (f313m false) (f313c 883) (f314m false) (f314c 663) (f315m false) (f315c 883) (f316m false) (f316c 0) (f317m true) (f317c (- 875)) (f318m true) (f318c 893) (f319m false) (f319c 0) (f320m false) (f320c (- 1)) (f321m false) (f321c 883) (f322m false) (f322c 0) (f323m false) (f323c 883) (f324m true) (f324c 546) (f325m true) (f325c (- 345)) (f326m false) (f326c 1004) (f327m true) (f327c 113) (f328m true) (f328c 661) (f329m false) (f329c 1004) (f330m false) (f330c 661) (f331m false) (f331c 1004) (f332m true) (f332c 657) (f333m true) (f333c (- 232)) (f334m true) (f334c 1143) (f335m true) (f335c 72) (f336m true) (f336c 661) (f337m false) (f337c 1665) (f338m false) (f338c 661) (f339m false) (f339c 1665) (f340m true) (f340c 573) (f341m true) (f341c (- 320)) (f342m true) (f342c 877) (f343m true) (f343c 166) (f344m true) (f344c 573) (f345m false) (f345c 881) (f346m false) (f346c 663) (f347m false) (f347c 881) (f348m true) (f348c 485) (f349m true) (f349c (- 226)) (f350m true) (f350c 611) (f351m true) (f351c (- 100)) (f352m true) (f352c 663) (f353m false) (f353c 883) (f354m false) (f354c 663) (f355m false) (f355c 883) (f356m false) (f356c 42) (f357m false) (f357c (- 961)) (f358m true) (f358c 925) (f359m true) (f359c (- 78)) (f360m true) (f360c 718) (f361m true) (f361c 1423) (f362m true) (f362c 696) (f363m true) (f363c 1422) (f364m true) (f364c 589) (f365m true) (f365c (- 425)) (f366m false) (f366c 1046) (f367m false) (f367c 43) (f368m true) (f368c 661) (f369m true) (f369c 1543) (f370m false) (f370c 661) (f371m true) (f371c 1544) (f372m true) (f372c 700) (f373m true) (f373c (- 314)) (f374m true) (f374c 1163) (f375m true) (f375c 164) (f376m true) (f376c 661) (f377m false) (f377c 1665) (f378m false) (f378c 661) (f379m false) (f379c 1665) (f380m true) (f380c 224) (f381m true) (f381c (- 663)) (f382m true) (f382c 1123) (f383m true) (f383c 238) (f384m true) (f384c 660) (f385m false) (f385c 1665) (f386m false) (f386c 661) (f387m false) (f387c 1665) (f388m true) (f388c 240) (f389m true) (f389c (- 679)) (f390m true) (f390c 1182) (f391m true) (f391c 220) (f392m false) (f392c 782) (f393m false) (f393c 1544) (f394m false) (f394c 782) (f395m false) (f395c 1544) (f396m true) (f396c 248) (f397m true) (f397c (- 671)) (f398m true) (f398c 1164) (f399m true) (f399c 202) (f400m false) (f400c 661) (f401m false) (f401c 1665) (f402m false) (f402c 661) (f403m false) (f403c 1665) (f404m true) (f404c (- 172)) (f405m true) (f405c (- 565)) (f406m true) (f406c 180) (f407m true) (f407c (- 172)) (f408m true) (f408c 663) (f409m false) (f409c 883) (f410m false) (f410c 663) (f411m false) (f411c 883) (f412m true) (f412c (- 260)) (f413m true) (f413c (- 842)) (f414m true) (f414c 48) (f415m true) (f415c (- 258)) (f416m true) (f416c 663) (f417m false) (f417c 883) (f418m false) (f418c 663) (f419m false) (f419c 883) (f420m true) (f420c (- 344)) (f421m true) (f421c (- 1156)) (f422m true) (f422c (- 40)) (f423m true) (f423c (- 522)) (f424m true) (f424c 663) (f425m false) (f425c 883) (f426m false) (f426c 663) (f427m false) (f427c 883) (f428m true) (f428c (- 432)) (f429m true) (f429c (- 1270)) (f430m true) (f430c (- 128)) (f431m true) (f431c (- 786)) (f432m true) (f432c 491) (f433m false) (f433c 883) (f434m false) (f434c 663) (f435m false) (f435c 883) (f436m true) (f436c (- 520)) (f437m true) (f437c (- 1360)) (f438m true) (f438c (- 212)) (f439m true) (f439c (- 1050)) (f440m true) (f440c 663) (f441m false) (f441c 883) (f442m false) (f442c 663) (f443m false) (f443c 883) (f444m false) (f444c 42) (f445m false) (f445c (- 961)) (f446m true) (f446c 530) (f447m true) (f447c (- 473)) (f448m true) (f448c 439) (f449m true) (f449c 1442) (f450m true) (f450c 696) (f451m true) (f451c 1000) (f452m true) (f452c (- 46)) (f453m true) (f453c (- 680)) (f454m false) (f454c 262) (f455m false) (f455c (- 741)) (f456m true) (f456c 608) (f457m true) (f457c 916) (f458m false) (f458c 663) (f459m true) (f459c 916) (f460m true) (f460c (- 134)) (f461m true) (f461c (- 766)) (f462m true) (f462c (- 6)) (f463m true) (f463c (- 1009)) (f464m true) (f464c 663) (f465m false) (f465c 883) (f466m false) (f466c 663) (f467m false) (f467c 883) (f468m true) (f468c (- 126)) (f469m true) (f469c (- 758)) (f470m true) (f470c (- 191)) (f471m true) (f471c (- 1029)) (f472m false) (f472c 0) (f473m false) (f473c 1546) (f474m false) (f474c 0) (f475m false) (f475c 1546) (f476m true) (f476c (- 1074)) (f477m true) (f477c (- 750)) (f478m true) (f478c (- 211)) (f479m true) (f479c (- 1049)) (f480m false) (f480c 663) (f481m false) (f481c 883) (f482m false) (f482c 663) (f483m false) (f483c 883) (f484m true) (f484c 222) (f485m true) (f485c (- 390)) (f486m true) (f486c 1123) (f487m true) (f487c 238) (f488m true) (f488c 660) (f489m false) (f489c 1665) (f490m false) (f490c 661) (f491m false) (f491c 1665) (f492m true) (f492c 230) (f493m true) (f493c (- 398)) (f494m true) (f494c 1105) (f495m true) (f495c 493) (f496m false) (f496c 782) (f497m false) (f497c 1544) (f498m false) (f498c 782) (f499m false) (f499c 1544) (f500m true) (f500c 238) (f501m true) (f501c (- 390)) (f502m true) (f502c 1113) (f503m true) (f503c 485) (f504m false) (f504c 661) (f505m false) (f505c 1665) (f506m false) (f506c 661) (f507m false) (f507c 1665) (f508m true) (f508c (- 172)) (f509m true) (f509c (- 660)) (f510m true) (f510c 286) (f511m true) (f511c (- 172)) (f512m true) (f512c 663) (f513m false) (f513c 883) (f514m false) (f514c 663) (f515m false) (f515c 883) (f516m true) (f516c (- 61)) (f517m true) (f517c (- 519)) (f518m true) (f518c 405) (f519m true) (f519c (- 53)) (f520m true) (f520c 662) (f521m false) (f521c 1667) (f522m false) (f522c 661) (f523m false) (f523c 1667) (f524m true) (f524c 58) (f525m true) (f525c (- 400)) (f526m true) (f526c 524) (f527m true) (f527c 485) (f528m true) (f528c 662) (f529m false) (f529c 1665) (f530m false) (f530c 661) (f531m false) (f531c 1665) (f532m true) (f532c 220) (f533m true) (f533c (- 226)) (f534m true) (f534c 1109) (f535m true) (f535c 238) (f536m true) (f536c 660) (f537m false) (f537c 1665) (f538m false) (f538c 661) (f539m false) (f539c 1665) (f540m true) (f540c 226) (f541m true) (f541c (- 216)) (f542m true) (f542c 1091) (f543m true) (f543c 657) (f544m false) (f544c 782) (f545m false) (f545c 1544) (f546m false) (f546c 782) (f547m false) (f547c 1544) (f548m true) (f548c 232) (f549m true) (f549c (- 206)) (f550m true) (f550c 1109) (f551m true) (f551c 667) (f552m false) (f552c 661) (f553m false) (f553c 1665) (f554m false) (f554c 661) (f555m false) (f555c 1665) (f556m true) (f556c 224) (f557m true) (f557c (- 236)) (f558m true) (f558c 1046) (f559m true) (f559c 1010) (f560m true) (f560c 656) (f561m false) (f561c 1665) (f562m false) (f562c 661) (f563m false) (f563c 1665) (f564m true) (f564c 138) (f565m true) (f565c (- 324)) (f566m true) (f566c 778) (f567m true) (f567c 744) (f568m true) (f568c 573) (f569m false) (f569c 881) (f570m false) (f570c 663) (f571m false) (f571c 881) (f572m true) (f572c 52) (f573m true) (f573c (- 411)) (f574m true) (f574c 512) (f575m true) (f575c 476) (f576m true) (f576c 489) (f577m false) (f577c 883) (f578m false) (f578c 663) (f579m false) (f579c 883) (f580m true) (f580c 165) (f581m true) (f581c (- 300)) (f582m true) (f582c 631) (f583m true) (f583c 593) (f584m true) (f584c 534) (f585m false) (f585c 1667) (f586m false) (f586c 661) (f587m false) (f587c 1667) (f588m true) (f588c 284) (f589m true) (f589c (- 189)) (f590m true) (f590c 750) (f591m true) (f591c 667) (f592m true) (f592c 770) (f593m false) (f593c 1665) (f594m false) (f594c 661) (f595m false) (f595c 1665) (f596m true) (f596c 220) (f597m true) (f597c (- 228)) (f598m true) (f598c 614) (f599m true) (f599c 238) (f600m true) (f600c 658) (f601m false) (f601c 1665) (f602m false) (f602c 661) (f603m false) (f603c 1665) (f604m true) (f604c (- 368)) (f605m true) (f605c (- 206)) (f606m true) (f606c 638) (f607m true) (f607c 259) (f608m false) (f608c 683) (f609m true) (f609c 1686) (f610m false) (f610c 683) (f611m true) (f611c 1422) (f612m true) (f612c (- 346)) (f613m true) (f613c (- 185)) (f614m true) (f614c (- 42)) (f615m true) (f615c 280) (f616m false) (f616c 704) (f617m true) (f617c 1443) (f618m false) (f618c 704) (f619m true) (f619c 1444) (f620m true) (f620c (- 924)) (f621m true) (f621c (- 177)) (f622m true) (f622c 537) (f623m true) (f623c 714) (f624m true) (f624c (- 1)) (f625m false) (f625c 1587) (f626m false) (f626c 0) (f627m false) (f627c 1587) (f628m true) (f628c (- 346)) (f629m true) (f629c (- 169)) (f630m true) (f630c (- 39)) (f631m true) (f631c 706) (f632m false) (f632c 704) (f633m false) (f633c 883) (f634m false) (f634c 704) (f635m false) (f635c 883) (f636m true) (f636c (- 174)) (f637m true) (f637c (- 1018)) (f638m true) (f638c 134) (f639m true) (f639c (- 532)) (f640m true) (f640c 662) (f641m false) (f641c 883) (f642m false) (f642c 663) (f643m false) (f643c 883) (f644m true) (f644c (- 258)) (f645m true) (f645c (- 924)) (f646m true) (f646c 46) (f647m true) (f647c (- 798)) (f648m true) (f648c 573) (f649m false) (f649c 883) (f650m false) (f650c 663) (f651m false) (f651c 883) (f652m true) (f652c (- 346)) (f653m true) (f653c (- 1190)) (f654m true) (f654c (- 38)) (f655m true) (f655c (- 704)) (f656m true) (f656c 575) (f657m false) (f657c 883) (f658m false) (f658c 663) (f659m false) (f659c 883))