sat ((f0m false) (f0c 31) (f1m true) (f1c 44) (f2m true) (f2c 0) (f3m true) (f3c (- 40)) (f4m true) (f4c 87) (f5m true) (f5c 29) (f6m false) (f6c 13) (f7m true) (f7c 26) (f8m false) (f8c 0) (f9m false) (f9c 13) (f10m true) (f10c 0) (f11m true) (f11c (- 14)) (f12m false) (f12c 0) (f13m false) (f13c 13) (f14m false) (f14c (- 13)) (f15m false) (f15c 0) (f16m true) (f16c 43) (f17m true) (f17c (- 13)) (f18m false) (f18c 18) (f19m false) (f19c 31) (f20m true) (f20c (- 17)) (f21m true) (f21c (- 8)) (f22m true) (f22c 17) (f23m true) (f23c 28) (f24m false) (f24c 7) (f25m true) (f25c 13) (f26m false) (f26c 0) (f27m false) (f27c 13) (f28m true) (f28c 3) (f29m true) (f29c (- 10)) (f30m false) (f30c 0) (f31m false) (f31c 44) (f32m true) (f32c (- 52)) (f33m true) (f33c 7) (f34m true) (f34c 96) (f35m true) (f35c 61) (f36m false) (f36c 13) (f37m true) (f37c 13) (f38m false) (f38c 0) (f39m false) (f39c 13) (f40m true) (f40c 25) (f41m true) (f41c 12) (f42m false) (f42c 0) (f43m false) (f43c 13) (f44m false) (f44c (- 13)) (f45m false) (f45c 0) (f46m true) (f46c 43) (f47m true) (f47c 30) (f48m true) (f48c 43) (f49m true) (f49c (- 13)) (f50m false) (f50c 13) (f51m false) (f51c 26) (f52m false) (f52c 0) (f53m false) (f53c 13) (f54m true) (f54c 0) (f55m true) (f55c 43) (f56m true) (f56c 0) (f57m true) (f57c 43) (f58m false) (f58c 44) (f59m false) (f59c 57) (f60m true) (f60c 13) (f61m true) (f61c 24) (f62m true) (f62c 87) (f63m true) (f63c 0) (f64m true) (f64c 87) (f65m true) (f65c 29) (f66m false) (f66c 14) (f67m true) (f67c 39) (f68m false) (f68c 13) (f69m false) (f69c 26) (f70m true) (f70c 11) (f71m true) (f71c (- 11)) (f72m true) (f72c 3) (f73m true) (f73c (- 10)) (f74m false) (f74c 26) (f75m false) (f75c 39) (f76m false) (f76c 13) (f77m false) (f77c 26) (f78m true) (f78c 3) (f79m true) (f79c 30) (f80m true) (f80c 43) (f81m true) (f81c 30) (f82m false) (f82c 44) (f83m false) (f83c 57) (f84m true) (f84c 10) (f85m true) (f85c 22) (f86m true) (f86c 61) (f87m true) (f87c 27) (f88m true) (f88c 61) (f89m true) (f89c 28) (f90m false) (f90c 26) (f91m true) (f91c 39) (f92m false) (f92c 13) (f93m false) (f93c 26) (f94m true) (f94c 25) (f95m true) (f95c 25) (f96m true) (f96c 25) (f97m true) (f97c 12) (f98m false) (f98c 39) (f99m true) (f99c 39) (f100m false) (f100c 26) (f101m false) (f101c 39) (f102m true) (f102c 25) (f103m true) (f103c 25) (f104m true) (f104c 25) (f105m true) (f105c 25) (f106m false) (f106c 52) (f107m true) (f107c 58) (f108m false) (f108c 39) (f109m false) (f109c 52) (f110m true) (f110c 38) (f111m true) (f111c 38) (f112m true) (f112c 25) (f113m true) (f113c 38) (f114m false) (f114c 65) (f115m true) (f115c 109) (f116m false) (f116c 52) (f117m false) (f117c 65) (f118m true) (f118c 51) (f119m true) (f119c 51) (f120m true) (f120c 25) (f121m true) (f121c 51) (f122m false) (f122c 96) (f123m false) (f123c 109) (f124m true) (f124c 55) (f125m true) (f125c 70) (f126m true) (f126c 95) (f127m true) (f127c 60) (f128m true) (f128c 96) (f129m true) (f129c 61) (f130m false) (f130c 14) (f131m true) (f131c 40) (f132m false) (f132c 13) (f133m false) (f133c 26) (f134m true) (f134c 3) (f135m true) (f135c 3) (f136m true) (f136c 3) (f137m true) (f137c 12) (f138m false) (f138c 27) (f139m true) (f139c 39) (f140m false) (f140c 26) (f141m false) (f141c 39) (f142m true) (f142c 25) (f143m true) (f143c 3) (f144m true) (f144c 25) (f145m true) (f145c 25) (f146m false) (f146c 40) (f147m true) (f147c 65) (f148m false) (f148c 39) (f149m false) (f149c 52) (f150m true) (f150c 38) (f151m true) (f151c 25) (f152m true) (f152c 38) (f153m true) (f153c 25) (f154m false) (f154c 53) (f155m true) (f155c 78) (f156m false) (f156c 52) (f157m false) (f157c 65) (f158m true) (f158c 51) (f159m true) (f159c 38) (f160m true) (f160c 0) (f161m true) (f161c 38) (f162m false) (f162c 84) (f163m true) (f163c 109) (f164m true) (f164c 53) (f165m true) (f165c 69) (f166m true) (f166c 87) (f167m true) (f167c 0) (f168m true) (f168c 87) (f169m true) (f169c 29) (f170m false) (f170c 14) (f171m true) (f171c 39) (f172m false) (f172c 13) (f173m false) (f173c 26) (f174m true) (f174c 3) (f175m true) (f175c 3) (f176m true) (f176c 3) (f177m true) (f177c 66) (f178m false) (f178c 26) (f179m false) (f179c 39) (f180m false) (f180c 13) (f181m false) (f181c 26) (f182m true) (f182c 79) (f183m true) (f183c 66) (f184m true) (f184c 79) (f185m true) (f185c 66) (f186m false) (f186c 44) (f187m false) (f187c 57) (f188m true) (f188c 10) (f189m true) (f189c 22) (f190m true) (f190c 97) (f191m true) (f191c 63) (f192m true) (f192c 97) (f193m true) (f193c 64) (f194m false) (f194c 0) (f195m false) (f195c 13) (f196m false) (f196c (- 13)) (f197m false) (f197c 0) (f198m true) (f198c 0) (f199m true) (f199c (- 13)) (f200m true) (f200c 43) (f201m true) (f201c (- 13)) (f202m false) (f202c 13) (f203m false) (f203c 26) (f204m false) (f204c 0) (f205m false) (f205c 13) (f206m true) (f206c 56) (f207m true) (f207c 0) (f208m true) (f208c 56) (f209m true) (f209c 0) (f210m false) (f210c 44) (f211m false) (f211c 57) (f212m true) (f212c (- 37)) (f213m true) (f213c 22) (f214m true) (f214c 44) (f215m true) (f215c 5) (f216m true) (f216c 96) (f217m true) (f217c 61) (f218m false) (f218c 14) (f219m true) (f219c 26) (f220m false) (f220c 13) (f221m false) (f221c 26) (f222m true) (f222c 11) (f223m true) (f223c 3) (f224m true) (f224c 1) (f225m true) (f225c (- 11)) (f226m false) (f226c 26) (f227m false) (f227c 39) (f228m false) (f228c 13) (f229m false) (f229c 26) (f230m true) (f230c 1) (f231m true) (f231c (- 11)) (f232m true) (f232c 1) (f233m true) (f233c (- 12)) (f234m false) (f234c 44) (f235m false) (f235c 57) (f236m true) (f236c 11) (f237m true) (f237c 24) (f238m true) (f238c 19) (f239m true) (f239c (- 15)) (f240m true) (f240c 19) (f241m true) (f241c 28) (f242m false) (f242c 0) (f243m false) (f243c 13) (f244m false) (f244c (- 13)) (f245m false) (f245c 0) (f246m true) (f246c 0) (f247m true) (f247c 30) (f248m true) (f248c 32) (f249m true) (f249c 30) (f250m false) (f250c 13) (f251m false) (f251c 26) (f252m false) (f252c 0) (f253m false) (f253c 13) (f254m true) (f254c 43) (f255m true) (f255c (- 14)) (f256m true) (f256c 10) (f257m true) (f257c (- 14)) (f258m false) (f258c 26) (f259m false) (f259c 39) (f260m false) (f260c 13) (f261m false) (f261c 26) (f262m true) (f262c (- 1)) (f263m true) (f263c (- 1)) (f264m true) (f264c (- 1)) (f265m true) (f265c (- 16)) (f266m false) (f266c 26) (f267m false) (f267c 39) (f268m false) (f268c 13) (f269m false) (f269c 26) (f270m true) (f270c (- 1)) (f271m true) (f271c (- 16)) (f272m true) (f272c (- 1)) (f273m true) (f273c (- 14)) (f274m false) (f274c 44) (f275m false) (f275c 57) (f276m true) (f276c 10) (f277m true) (f277c 24) (f278m true) (f278c 17) (f279m true) (f279c (- 17)) (f280m true) (f280c 17) (f281m true) (f281c 28) (f282m false) (f282c 14) (f283m true) (f283c 26) (f284m false) (f284c 13) (f285m false) (f285c 26) (f286m true) (f286c 3) (f287m true) (f287c 3) (f288m true) (f288c 43) (f289m true) (f289c 30) (f290m false) (f290c 26) (f291m false) (f291c 39) (f292m false) (f292c 13) (f293m false) (f293c 26) (f294m true) (f294c 43) (f295m true) (f295c 30) (f296m true) (f296c 43) (f297m true) (f297c 30) (f298m false) (f298c 44) (f299m false) (f299c 57) (f300m true) (f300c 5) (f301m true) (f301c 22) (f302m true) (f302c 61) (f303m true) (f303c 26) (f304m true) (f304c 61) (f305m true) (f305c 28) (f306m false) (f306c 0) (f307m false) (f307c 13) (f308m false) (f308c (- 13)) (f309m false) (f309c 0) (f310m true) (f310c 0) (f311m true) (f311c (- 13)) (f312m true) (f312c 0) (f313m true) (f313c (- 13)) (f314m false) (f314c 13) (f315m false) (f315c 26) (f316m false) (f316c 0) (f317m false) (f317c 13) (f318m true) (f318c 13) (f319m true) (f319c 12) (f320m true) (f320c 25) (f321m true) (f321c 12) (f322m false) (f322c 26) (f323m false) (f323c 39) (f324m false) (f324c 13) (f325m false) (f325c 26) (f326m true) (f326c 25) (f327m true) (f327c 25) (f328m true) (f328c 25) (f329m true) (f329c 25) (f330m false) (f330c 44) (f331m false) (f331c 57) (f332m true) (f332c 9) (f333m true) (f333c 18) (f334m true) (f334c 56) (f335m true) (f335c 18) (f336m true) (f336c 56) (f337m true) (f337c 28) (f338m false) (f338c 14) (f339m true) (f339c 26) (f340m false) (f340c 13) (f341m false) (f341c 26) (f342m true) (f342c 3) (f343m true) (f343c (- 11)) (f344m true) (f344c 3) (f345m true) (f345c (- 10)) (f346m false) (f346c 26) (f347m false) (f347c 39) (f348m false) (f348c 13) (f349m false) (f349c 26) (f350m true) (f350c 3) (f351m true) (f351c (- 10)) (f352m true) (f352c 3) (f353m true) (f353c (- 10)) (f354m false) (f354c 44) (f355m false) (f355c 57) (f356m true) (f356c 7) (f357m true) (f357c 18) (f358m true) (f358c 21) (f359m true) (f359c (- 13)) (f360m true) (f360c 21) (f361m true) (f361c 28) (f362m false) (f362c 0) (f363m false) (f363c 13) (f364m false) (f364c (- 13)) (f365m false) (f365c 0) (f366m true) (f366c 0) (f367m true) (f367c (- 13)) (f368m true) (f368c 43) (f369m true) (f369c (- 13)) (f370m false) (f370c 13) (f371m false) (f371c 26) (f372m false) (f372c 0) (f373m false) (f373c 13) (f374m true) (f374c 56) (f375m true) (f375c 12) (f376m true) (f376c 56) (f377m true) (f377c 12) (f378m false) (f378c 44) (f379m false) (f379c 57) (f380m true) (f380c 6) (f381m true) (f381c (- 28)) (f382m true) (f382c 56) (f383m true) (f383c 18) (f384m true) (f384c 96) (f385m true) (f385c 17) (f386m false) (f386c 26) (f387m true) (f387c 26) (f388m false) (f388c 13) (f389m false) (f389c 26) (f390m true) (f390c 38) (f391m true) (f391c 10) (f392m true) (f392c 38) (f393m true) (f393c 27) (f394m false) (f394c 26) (f395m false) (f395c 39) (f396m false) (f396c 13) (f397m false) (f397c 26) (f398m true) (f398c 42) (f399m true) (f399c 25) (f400m true) (f400c 43) (f401m true) (f401c 24) (f402m false) (f402c 26) (f403m false) (f403c 39) (f404m false) (f404c 13) (f405m false) (f405c 26) (f406m true) (f406c 43) (f407m true) (f407c 24) (f408m true) (f408c 43) (f409m true) (f409c 24) (f410m false) (f410c 39) (f411m false) (f411c 52) (f412m false) (f412c 26) (f413m false) (f413c 39) (f414m true) (f414c 37) (f415m true) (f415c 37) (f416m true) (f416c 26) (f417m true) (f417c 17) (f418m false) (f418c 52) (f419m false) (f419c 65) (f420m false) (f420c 39) (f421m false) (f421c 52) (f422m true) (f422c 27) (f423m true) (f423c 28) (f424m true) (f424c 25) (f425m true) (f425c 28) (f426m false) (f426c 26) (f427m true) (f427c 26) (f428m false) (f428c 13) (f429m false) (f429c 26) (f430m true) (f430c 25) (f431m true) (f431c 25) (f432m true) (f432c 24) (f433m true) (f433c 25) (f434m false) (f434c 26) (f435m false) (f435c 39) (f436m false) (f436c 13) (f437m false) (f437c 26) (f438m true) (f438c 22) (f439m true) (f439c 25) (f440m true) (f440c 21) (f441m true) (f441c 25) (f442m false) (f442c 26) (f443m false) (f443c 39) (f444m false) (f444c 13) (f445m false) (f445c 26) (f446m true) (f446c 19) (f447m true) (f447c 25) (f448m true) (f448c (- 3)) (f449m true) (f449c (- 9)) (f450m false) (f450c 33) (f451m false) (f451c 46) (f452m false) (f452c 26) (f453m false) (f453c 39) (f454m true) (f454c 4) (f455m true) (f455c (- 5)) (f456m true) (f456c 4) (f457m true) (f457c (- 10)) (f458m false) (f458c 40) (f459m false) (f459c 53) (f460m false) (f460c 39) (f461m false) (f461c 52) (f462m true) (f462c 3) (f463m true) (f463c 3) (f464m true) (f464c 3) (f465m true) (f465c 4) (f466m false) (f466c 0) (f467m false) (f467c 13) (f468m false) (f468c (- 13)) (f469m false) (f469c 0) (f470m true) (f470c 43) (f471m true) (f471c 30) (f472m true) (f472c 43) (f473m true) (f473c 30) (f474m false) (f474c 13) (f475m false) (f475c 26) (f476m false) (f476c 0) (f477m false) (f477c 13) (f478m true) (f478c 56) (f479m true) (f479c 43) (f480m true) (f480c 56) (f481m true) (f481c 43) (f482m false) (f482c 26) (f483m false) (f483c 39) (f484m false) (f484c 13) (f485m false) (f485c 26) (f486m true) (f486c 69) (f487m true) (f487c 56) (f488m true) (f488c 69) (f489m true) (f489c 56) (f490m false) (f490c 14) (f491m true) (f491c 26) (f492m false) (f492c 13) (f493m false) (f493c 26) (f494m true) (f494c 10) (f495m true) (f495c 3) (f496m true) (f496c 10) (f497m true) (f497c (- 10)) (f498m false) (f498c 26) (f499m false) (f499c 39) (f500m false) (f500c 13) (f501m false) (f501c 26) (f502m true) (f502c 43) (f503m true) (f503c 30) (f504m true) (f504c 43) (f505m true) (f505c 30) (f506m false) (f506c 26) (f507m false) (f507c 39) (f508m false) (f508c 13) (f509m false) (f509c 26) (f510m true) (f510c 43) (f511m true) (f511c 30) (f512m true) (f512c 43) (f513m true) (f513c 30) (f514m false) (f514c 26) (f515m true) (f515c 26) (f516m false) (f516c 13) (f517m false) (f517c 26) (f518m true) (f518c 25) (f519m true) (f519c 27) (f520m true) (f520c 25) (f521m true) (f521c 12) (f522m false) (f522c 39) (f523m true) (f523c 39) (f524m false) (f524c 26) (f525m false) (f525c 39) (f526m true) (f526c 40) (f527m true) (f527c 25) (f528m true) (f528c 41) (f529m true) (f529c 12) (f530m false) (f530c 52) (f531m true) (f531c 52) (f532m false) (f532c 39) (f533m false) (f533c 52) (f534m true) (f534c 25) (f535m true) (f535c 31) (f536m true) (f536c 25) (f537m true) (f537c 32) (f538m false) (f538c 65) (f539m true) (f539c 65) (f540m false) (f540c 52) (f541m false) (f541c 65) (f542m true) (f542c 38) (f543m true) (f543c 46) (f544m true) (f544c 60) (f545m true) (f545c 47) (f546m false) (f546c 78) (f547m true) (f547c 78) (f548m false) (f548c 65) (f549m false) (f549c 78) (f550m true) (f550c 60) (f551m true) (f551c 60) (f552m true) (f552c 25) (f553m true) (f553c 52) (f554m false) (f554c 14) (f555m true) (f555c 39) (f556m false) (f556c 13) (f557m false) (f557c 26) (f558m true) (f558c 11) (f559m true) (f559c 3) (f560m true) (f560c 11) (f561m true) (f561c (- 10)) (f562m false) (f562c 27) (f563m true) (f563c 52) (f564m false) (f564c 26) (f565m false) (f565c 39) (f566m true) (f566c 25) (f567m true) (f567c 12) (f568m true) (f568c 25) (f569m true) (f569c 12) (f570m false) (f570c 40) (f571m true) (f571c 65) (f572m false) (f572c 39) (f573m false) (f573c 52) (f574m true) (f574c 25) (f575m true) (f575c 26) (f576m true) (f576c 25) (f577m true) (f577c 26) (f578m false) (f578c 53) (f579m true) (f579c 78) (f580m false) (f580c 52) (f581m false) (f581c 65) (f582m true) (f582c 52) (f583m true) (f583c 39) (f584m true) (f584c 52) (f585m true) (f585c 39) (f586m false) (f586c 66) (f587m true) (f587c 78) (f588m false) (f588c 65) (f589m false) (f589c 78) (f590m true) (f590c 0) (f591m true) (f591c 52) (f592m true) (f592c 0) (f593m true) (f593c 52) (f594m false) (f594c 14) (f595m true) (f595c 26) (f596m false) (f596c 13) (f597m false) (f597c 26) (f598m true) (f598c 3) (f599m true) (f599c 3) (f600m true) (f600c 3) (f601m true) (f601c 30) (f602m false) (f602c 26) (f603m false) (f603c 39) (f604m false) (f604c 13) (f605m false) (f605c 26) (f606m true) (f606c 3) (f607m true) (f607c 30) (f608m true) (f608c 43) (f609m true) (f609c 30) (f610m false) (f610c 26) (f611m false) (f611c 39) (f612m false) (f612c 13) (f613m false) (f613c 26) (f614m true) (f614c 43) (f615m true) (f615c 30) (f616m true) (f616c 43) (f617m true) (f617c 30) (f618m false) (f618c 0) (f619m false) (f619c 13) (f620m false) (f620c (- 13)) (f621m false) (f621c 0) (f622m true) (f622c 43) (f623m true) (f623c (- 13)) (f624m true) (f624c 43) (f625m true) (f625c (- 13)) (f626m false) (f626c 13) (f627m false) (f627c 26) (f628m false) (f628c 0) (f629m false) (f629c 13) (f630m true) (f630c 56) (f631m true) (f631c (- 1)) (f632m true) (f632c 12) (f633m true) (f633c 12) (f634m false) (f634c 26) (f635m false) (f635c 39) (f636m false) (f636c 13) (f637m false) (f637c 26) (f638m true) (f638c 25) (f639m true) (f639c 12) (f640m true) (f640c 25) (f641m true) (f641c 12) (f642m false) (f642c 14) (f643m true) (f643c 20) (f644m false) (f644c 13) (f645m false) (f645c 26) (f646m true) (f646c 3) (f647m true) (f647c 3) (f648m true) (f648c 3) (f649m true) (f649c 30) (f650m false) (f650c 26) (f651m false) (f651c 39) (f652m false) (f652c 13) (f653m false) (f653c 26) (f654m true) (f654c 43) (f655m true) (f655c 30) (f656m true) (f656c 43) (f657m true) (f657c 30) (f658m false) (f658c 26) (f659m false) (f659c 39) (f660m false) (f660c 13) (f661m false) (f661c 26) (f662m true) (f662c 43) (f663m true) (f663c 30) (f664m true) (f664c 43) (f665m true) (f665c 30) (f666m false) (f666c 0) (f667m false) (f667c 13) (f668m false) (f668c (- 13)) (f669m false) (f669c 0) (f670m true) (f670c 43) (f671m true) (f671c (- 13)) (f672m true) (f672c 43) (f673m true) (f673c (- 13)) (f674m false) (f674c 13) (f675m false) (f675c 26) (f676m false) (f676c 0) (f677m false) (f677c 13) (f678m true) (f678c 56) (f679m true) (f679c 43) (f680m true) (f680c 25) (f681m true) (f681c 43) (f682m false) (f682c 26) (f683m false) (f683c 39) (f684m false) (f684c 13) (f685m false) (f685c 26) (f686m true) (f686c 38) (f687m true) (f687c 12) (f688m true) (f688c 38) (f689m true) (f689c 12) (f690m false) (f690c 26) (f691m false) (f691c 39) (f692m false) (f692c 13) (f693m false) (f693c 26) (f694m true) (f694c 38) (f695m true) (f695c (- 13)) (f696m true) (f696c 38) (f697m true) (f697c (- 13)) (f698m false) (f698c 26) (f699m false) (f699c 39) (f700m false) (f700c 13) (f701m false) (f701c 26) (f702m true) (f702c 38) (f703m true) (f703c (- 13)) (f704m true) (f704c 38) (f705m true) (f705c (- 13)) (f706m false) (f706c 14) (f707m true) (f707c 26) (f708m false) (f708c 13) (f709m false) (f709c 26) (f710m true) (f710c 3) (f711m true) (f711c 3) (f712m true) (f712c 3) (f713m true) (f713c (- 10)) (f714m false) (f714c 27) (f715m true) (f715c 53) (f716m false) (f716c 26) (f717m false) (f717c 39) (f718m true) (f718c 16) (f719m true) (f719c 3) (f720m true) (f720c 0) (f721m true) (f721c 3) (f722m false) (f722c 40) (f723m true) (f723c 65) (f724m false) (f724c 39) (f725m false) (f725c 52) (f726m true) (f726c 13) (f727m true) (f727c (- 13)) (f728m true) (f728c 0) (f729m true) (f729c (- 13)) (f730m false) (f730c 52) (f731m false) (f731c 65) (f732m false) (f732c 39) (f733m false) (f733c 52) (f734m true) (f734c 0) (f735m true) (f735c (- 13)) (f736m true) (f736c 0) (f737m true) (f737c (- 13)) (f738m false) (f738c 52) (f739m false) (f739c 65) (f740m false) (f740c 39) (f741m false) (f741c 52) (f742m true) (f742c 43) (f743m true) (f743c (- 13)) (f744m true) (f744c 43) (f745m true) (f745c (- 13)) (f746m false) (f746c 26) (f747m true) (f747c 26) (f748m false) (f748c 13) (f749m false) (f749c 26) (f750m true) (f750c 38) (f751m true) (f751c 25) (f752m true) (f752c (- 26)) (f753m true) (f753c 25) (f754m false) (f754c 39) (f755m true) (f755c 39) (f756m false) (f756c 26) (f757m false) (f757c 39) (f758m true) (f758c (- 13)) (f759m true) (f759c 38) (f760m true) (f760c (- 13)) (f761m true) (f761c 12) (f762m false) (f762c 52) (f763m true) (f763c 52) (f764m false) (f764c 39) (f765m false) (f765c 52) (f766m true) (f766c 25) (f767m true) (f767c (- 13)) (f768m true) (f768c 25) (f769m true) (f769c (- 13)))