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