sat ((f0m true) (f0c 21) (f1m false) (f1c (- 21)) (f2m true) (f2c 0) (f3m true) (f3c 58) (f4m false) (f4c 0) (f5m true) (f5c 79) (f6m false) (f6c (- 21)) (f7m false) (f7c (- 42)) (f8m false) (f8c 0) (f9m true) (f9c (- 64)) (f10m false) (f10c 0) (f11m false) (f11c 13) (f12m true) (f12c (- 16)) (f13m false) (f13c 0) (f14m true) (f14c 7) (f15m false) (f15c 0) (f16m false) (f16c 20) (f17m false) (f17c 22) (f18m true) (f18c 9) (f19m false) (f19c 0) (f20m true) (f20c 50) (f21m false) (f21c 0) (f22m false) (f22c 22) (f23m false) (f23c 22) (f24m false) (f24c 22) (f25m false) (f25c 22) (f26m true) (f26c 8) (f27m false) (f27c (- 21)) (f28m true) (f28c 9) (f29m false) (f29c 0) (f30m false) (f30c 1) (f31m false) (f31c 22) (f32m false) (f32c 1) (f33m false) (f33c 22) (f34m true) (f34c 31) (f35m false) (f35c (- 21)) (f36m true) (f36c 113) (f37m true) (f37c 58) (f38m false) (f38c 1) (f39m true) (f39c 80) (f40m false) (f40c 1) (f41m true) (f41c 80) (f42m true) (f42c (- 39)) (f43m false) (f43c (- 21)) (f44m true) (f44c 63) (f45m false) (f45c 0) (f46m false) (f46c (- 1)) (f47m false) (f47c 20) (f48m false) (f48c 0) (f49m false) (f49c 20) (f50m true) (f50c (- 57)) (f51m false) (f51c 0) (f52m true) (f52c 61) (f53m false) (f53c 0) (f54m false) (f54c 20) (f55m false) (f55c 20) (f56m false) (f56c 20) (f57m false) (f57c 22) (f58m true) (f58c (- 75)) (f59m false) (f59c 0) (f60m true) (f60c 58) (f61m false) (f61c 0) (f62m false) (f62c 22) (f63m false) (f63c 22) (f64m false) (f64c 22) (f65m false) (f65c 22) (f66m true) (f66c 58) (f67m false) (f67c 0) (f68m true) (f68c 55) (f69m false) (f69c 0) (f70m false) (f70c 22) (f71m false) (f71c 22) (f72m false) (f72c 22) (f73m false) (f73c 22) (f74m true) (f74c 32) (f75m false) (f75c (- 21)) (f76m true) (f76c 113) (f77m true) (f77c 58) (f78m false) (f78c 1) (f79m true) (f79c 80) (f80m false) (f80c 1) (f81m true) (f81c 80) (f82m true) (f82c 9) (f83m false) (f83c 0) (f84m true) (f84c (- 9)) (f85m false) (f85c 0) (f86m false) (f86c 22) (f87m false) (f87c 22) (f88m false) (f88c 22) (f89m false) (f89c 22) (f90m true) (f90c (- 51)) (f91m false) (f91c (- 21)) (f92m true) (f92c (- 63)) (f93m false) (f93c 0) (f94m false) (f94c 1) (f95m false) (f95c 22) (f96m false) (f96c 1) (f97m false) (f97c 22) (f98m true) (f98c (- 30)) (f99m false) (f99c (- 21)) (f100m true) (f100c (- 5)) (f101m true) (f101c 58) (f102m false) (f102c 1) (f103m true) (f103c 80) (f104m false) (f104c 1) (f105m true) (f105c 80) (f106m true) (f106c (- 35)) (f107m false) (f107c (- 21)) (f108m true) (f108c (- 59)) (f109m false) (f109c 0) (f110m false) (f110c (- 1)) (f111m false) (f111c 20) (f112m false) (f112c 0) (f113m false) (f113c 20) (f114m true) (f114c (- 51)) (f115m false) (f115c 0) (f116m true) (f116c (- 61)) (f117m false) (f117c 0) (f118m false) (f118c 20) (f119m false) (f119c 20) (f120m false) (f120c 20) (f121m false) (f121c 22) (f122m true) (f122c (- 107)) (f123m false) (f123c 0) (f124m true) (f124c (- 63)) (f125m false) (f125c 0) (f126m false) (f126c 22) (f127m false) (f127c 22) (f128m false) (f128c 22) (f129m false) (f129c 22) (f130m true) (f130c (- 86)) (f131m false) (f131c (- 21)) (f132m true) (f132c (- 5)) (f133m true) (f133c 58) (f134m false) (f134c 1) (f135m true) (f135c 80) (f136m false) (f136c 1) (f137m true) (f137c 80) (f138m true) (f138c 9) (f139m false) (f139c 0) (f140m true) (f140c (- 62)) (f141m false) (f141c 0) (f142m false) (f142c 22) (f143m false) (f143c 22) (f144m false) (f144c 22) (f145m false) (f145c 22) (f146m true) (f146c (- 104)) (f147m false) (f147c (- 21)) (f148m true) (f148c (- 62)) (f149m false) (f149c 0) (f150m false) (f150c 1) (f151m false) (f151c 22) (f152m false) (f152c 1) (f153m false) (f153c 22) (f154m true) (f154c (- 83)) (f155m false) (f155c (- 21)) (f156m true) (f156c (- 2)) (f157m true) (f157c 58) (f158m false) (f158c 1) (f159m true) (f159c 80) (f160m false) (f160c 1) (f161m true) (f161c 80) (f162m true) (f162c (- 37)) (f163m false) (f163c (- 21)) (f164m true) (f164c (- 57)) (f165m false) (f165c 0) (f166m false) (f166c (- 1)) (f167m false) (f167c 20) (f168m false) (f168c 0) (f169m false) (f169c 20) (f170m true) (f170c (- 53)) (f171m false) (f171c 0) (f172m true) (f172c (- 57)) (f173m false) (f173c 0) (f174m false) (f174c 20) (f175m false) (f175c 20) (f176m false) (f176c 20) (f177m false) (f177c 22) (f178m true) (f178c (- 32)) (f179m false) (f179c (- 21)) (f180m true) (f180c (- 1)) (f181m true) (f181c 58) (f182m false) (f182c 1) (f183m true) (f183c 80) (f184m false) (f184c 1) (f185m true) (f185c 80) (f186m true) (f186c (- 61)) (f187m false) (f187c 0) (f188m true) (f188c 5) (f189m false) (f189c 0) (f190m false) (f190c 22) (f191m false) (f191c 22) (f192m false) (f192c 22) (f193m false) (f193c 22) (f194m true) (f194c (- 82)) (f195m false) (f195c (- 21)) (f196m true) (f196c (- 61)) (f197m false) (f197c 0) (f198m false) (f198c 1) (f199m false) (f199c 22) (f200m false) (f200c 1) (f201m false) (f201c 22) (f202m true) (f202c (- 82)) (f203m false) (f203c (- 21)) (f204m true) (f204c (- 33)) (f205m true) (f205c 58) (f206m false) (f206c 1) (f207m true) (f207c 80) (f208m false) (f208c 1) (f209m true) (f209c 80) (f210m true) (f210c (- 35)) (f211m false) (f211c (- 21)) (f212m true) (f212c (- 16)) (f213m false) (f213c 0) (f214m false) (f214c (- 1)) (f215m false) (f215c 20) (f216m false) (f216c 0) (f217m false) (f217c 20) (f218m true) (f218c (- 14)) (f219m false) (f219c (- 21)) (f220m true) (f220c (- 34)) (f221m true) (f221c 58) (f222m false) (f222c (- 1)) (f223m true) (f223c 80) (f224m false) (f224c 0) (f225m true) (f225c 80) (f226m true) (f226c (- 32)) (f227m false) (f227c 0) (f228m true) (f228c 7) (f229m false) (f229c 0) (f230m false) (f230c 22) (f231m false) (f231c 22) (f232m false) (f232c 22) (f233m false) (f233c 22) (f234m true) (f234c (- 53)) (f235m false) (f235c (- 21)) (f236m true) (f236c (- 57)) (f237m false) (f237c 0) (f238m false) (f238c 1) (f239m false) (f239c 22) (f240m false) (f240c 1) (f241m false) (f241c 22) (f242m true) (f242c (- 32)) (f243m false) (f243c (- 21)) (f244m true) (f244c 1) (f245m true) (f245c 58) (f246m false) (f246c 1) (f247m true) (f247c 80) (f248m false) (f248c 1) (f249m true) (f249c 80) (f250m true) (f250c (- 37)) (f251m false) (f251c (- 21)) (f252m true) (f252c (- 55)) (f253m false) (f253c 0) (f254m false) (f254c (- 1)) (f255m false) (f255c 20) (f256m false) (f256c 0) (f257m false) (f257c 20) (f258m true) (f258c (- 53)) (f259m false) (f259c 0) (f260m true) (f260c (- 30)) (f261m false) (f261c 0) (f262m false) (f262c 20) (f263m false) (f263c 20) (f264m false) (f264c 20) (f265m false) (f265c 22) (f266m true) (f266c (- 32)) (f267m false) (f267c (- 21)) (f268m true) (f268c 49) (f269m true) (f269c 59) (f270m false) (f270c 1) (f271m true) (f271c 80) (f272m false) (f272c 1) (f273m true) (f273c 81) (f274m true) (f274c (- 32)) (f275m false) (f275c 0) (f276m true) (f276c (- 9)) (f277m false) (f277c 0) (f278m false) (f278c 22) (f279m false) (f279c 22) (f280m false) (f280c 22) (f281m false) (f281c 22) (f282m true) (f282c (- 32)) (f283m false) (f283c (- 21)) (f284m true) (f284c 49) (f285m true) (f285c 58) (f286m false) (f286c 1) (f287m true) (f287c 80) (f288m false) (f288c 1) (f289m true) (f289c 80) (f290m true) (f290c (- 41)) (f291m false) (f291c (- 21)) (f292m true) (f292c (- 57)) (f293m false) (f293c 0) (f294m false) (f294c (- 1)) (f295m false) (f295c 20) (f296m false) (f296c 0) (f297m false) (f297c 20) (f298m true) (f298c (- 57)) (f299m false) (f299c 0) (f300m true) (f300c (- 34)) (f301m false) (f301c 0) (f302m false) (f302c 20) (f303m false) (f303c 20) (f304m false) (f304c 20) (f305m false) (f305c 22) (f306m true) (f306c (- 36)) (f307m false) (f307c (- 21)) (f308m true) (f308c 24) (f309m true) (f309c 60) (f310m false) (f310c 1) (f311m true) (f311c 80) (f312m false) (f312c 1) (f313m true) (f313c 80) (f314m true) (f314c 5) (f315m false) (f315c (- 21)) (f316m true) (f316c 24) (f317m true) (f317c 56) (f318m false) (f318c 1) (f319m true) (f319c 80) (f320m false) (f320c 1) (f321m true) (f321c 80) (f322m true) (f322c (- 41)) (f323m false) (f323c (- 21)) (f324m true) (f324c (- 57)) (f325m false) (f325c 0) (f326m false) (f326c (- 1)) (f327m false) (f327c 20) (f328m false) (f328c 0) (f329m false) (f329c 20) (f330m true) (f330c (- 57)) (f331m false) (f331c 0) (f332m true) (f332c (- 34)) (f333m false) (f333c 0) (f334m false) (f334c 20) (f335m false) (f335c 20) (f336m false) (f336c 20) (f337m false) (f337c 22) (f338m true) (f338c (- 55)) (f339m false) (f339c (- 21)) (f340m true) (f340c 24) (f341m true) (f341c 58) (f342m false) (f342c 1) (f343m true) (f343c 80) (f344m false) (f344c 1) (f345m true) (f345c 80) (f346m true) (f346c (- 32)) (f347m false) (f347c 0) (f348m true) (f348c 9) (f349m false) (f349c 0) (f350m false) (f350c 22) (f351m false) (f351c 22) (f352m false) (f352c 22) (f353m false) (f353c 22) (f354m true) (f354c (- 11)) (f355m false) (f355c (- 21)) (f356m true) (f356c 67) (f357m true) (f357c 37) (f358m false) (f358c 1) (f359m true) (f359c 80) (f360m false) (f360c 1) (f361m true) (f361c 80) (f362m true) (f362c (- 32)) (f363m false) (f363c 0) (f364m true) (f364c 7) (f365m false) (f365c 0) (f366m false) (f366c 22) (f367m false) (f367c 22) (f368m false) (f368c 22) (f369m false) (f369c 22) (f370m true) (f370c (- 35)) (f371m false) (f371c (- 21)) (f372m true) (f372c (- 59)) (f373m false) (f373c 0) (f374m false) (f374c 1) (f375m false) (f375c 22) (f376m false) (f376c 1) (f377m false) (f377c 22) (f378m true) (f378c (- 56)) (f379m false) (f379c (- 42)) (f380m true) (f380c (- 123)) (f381m false) (f381c (- 21)) (f382m false) (f382c (- 20)) (f383m false) (f383c 1) (f384m false) (f384c 0) (f385m false) (f385c 13) (f386m true) (f386c (- 72)) (f387m false) (f387c (- 21)) (f388m true) (f388c (- 49)) (f389m false) (f389c (- 21)) (f390m false) (f390c 13) (f391m false) (f391c 13) (f392m false) (f392c 20) (f393m false) (f393c 22) (f394m true) (f394c (- 91)) (f395m false) (f395c (- 42)) (f396m true) (f396c (- 113)) (f397m false) (f397c (- 21)) (f398m false) (f398c (- 1)) (f399m false) (f399c 20) (f400m false) (f400c 0) (f401m false) (f401c 20) (f402m true) (f402c (- 70)) (f403m false) (f403c (- 42)) (f404m true) (f404c 67) (f405m true) (f405c 37) (f406m false) (f406c (- 1)) (f407m true) (f407c 78) (f408m false) (f408c 0) (f409m true) (f409c 80) (f410m true) (f410c 9) (f411m false) (f411c 0) (f412m true) (f412c 9) (f413m false) (f413c 0) (f414m false) (f414c 22) (f415m false) (f415c 22) (f416m false) (f416c 22) (f417m false) (f417c 22) (f418m true) (f418c (- 16)) (f419m false) (f419c (- 21)) (f420m true) (f420c 67) (f421m true) (f421c 58) (f422m false) (f422c 1) (f423m true) (f423c 80) (f424m false) (f424c 1) (f425m true) (f425c 80) (f426m true) (f426c (- 16)) (f427m false) (f427c (- 21)) (f428m true) (f428c 67) (f429m true) (f429c 58) (f430m false) (f430c 1) (f431m true) (f431c 80) (f432m false) (f432c 1) (f433m true) (f433c 80) (f434m true) (f434c (- 32)) (f435m false) (f435c 0) (f436m true) (f436c (- 9)) (f437m false) (f437c 0) (f438m false) (f438c 22) (f439m false) (f439c 22) (f440m false) (f440c 22) (f441m false) (f441c 22) (f442m true) (f442c (- 30)) (f443m false) (f443c (- 21)) (f444m true) (f444c 49) (f445m true) (f445c 58) (f446m false) (f446c 1) (f447m true) (f447c 80) (f448m false) (f448c 1) (f449m true) (f449c 80) (f450m true) (f450c (- 32)) (f451m false) (f451c 0) (f452m true) (f452c (- 12)) (f453m false) (f453c 0) (f454m false) (f454c 22) (f455m false) (f455c 22) (f456m false) (f456c 22) (f457m false) (f457c 22) (f458m true) (f458c (- 53)) (f459m false) (f459c (- 21)) (f460m true) (f460c (- 76)) (f461m false) (f461c 0) (f462m false) (f462c 1) (f463m false) (f463c 22) (f464m false) (f464c 1) (f465m false) (f465c 22) (f466m true) (f466c (- 76)) (f467m false) (f467c 0) (f468m true) (f468c (- 76)) (f469m false) (f469c 0) (f470m false) (f470c 22) (f471m false) (f471c 22) (f472m false) (f472c 22) (f473m false) (f473c 22) (f474m true) (f474c (- 35)) (f475m false) (f475c (- 21)) (f476m true) (f476c (- 57)) (f477m false) (f477c 0) (f478m false) (f478c (- 1)) (f479m false) (f479c 20) (f480m false) (f480c 0) (f481m false) (f481c 20) (f482m true) (f482c (- 51)) (f483m false) (f483c 0) (f484m true) (f484c (- 28)) (f485m false) (f485c 0) (f486m false) (f486c 20) (f487m false) (f487c 20) (f488m false) (f488c 20) (f489m false) (f489c 22) (f490m true) (f490c (- 67)) (f491m false) (f491c 0) (f492m true) (f492c (- 28)) (f493m false) (f493c 0) (f494m false) (f494c 22) (f495m false) (f495c 22) (f496m false) (f496c 22) (f497m false) (f497c 22) (f498m true) (f498c (- 83)) (f499m false) (f499c 0) (f500m true) (f500c (- 76)) (f501m false) (f501c 0) (f502m false) (f502c 22) (f503m false) (f503c 22) (f504m false) (f504c 22) (f505m false) (f505c 22) (f506m true) (f506c (- 76)) (f507m false) (f507c 0) (f508m true) (f508c (- 76)) (f509m false) (f509c 0) (f510m false) (f510c 22) (f511m false) (f511c 22) (f512m false) (f512c 22) (f513m false) (f513c 22) (f514m true) (f514c 25) (f515m false) (f515c (- 21)) (f516m true) (f516c 25) (f517m false) (f517c 0) (f518m false) (f518c (- 1)) (f519m false) (f519c 20) (f520m false) (f520c 0) (f521m false) (f521c 20) (f522m true) (f522c 23) (f523m false) (f523c 0) (f524m true) (f524c 30) (f525m false) (f525c 0) (f526m false) (f526c 20) (f527m false) (f527c 20) (f528m false) (f528c 20) (f529m false) (f529c 22) (f530m true) (f530c 7) (f531m false) (f531c 0) (f532m true) (f532c 30) (f533m false) (f533c 0) (f534m false) (f534c 22) (f535m false) (f535c 22) (f536m false) (f536c 22) (f537m false) (f537c 22) (f538m true) (f538c 23) (f539m false) (f539c 0) (f540m true) (f540c 7) (f541m false) (f541c 0) (f542m false) (f542c 22) (f543m false) (f543c 22) (f544m false) (f544c 22) (f545m false) (f545c 22) (f546m true) (f546c 7) (f547m false) (f547c 0) (f548m true) (f548c 7) (f549m false) (f549c 0) (f550m false) (f550c 22) (f551m false) (f551c 22) (f552m false) (f552c 22) (f553m false) (f553c 22) (f554m true) (f554c 7) (f555m false) (f555c 0) (f556m true) (f556c 7) (f557m false) (f557c 0) (f558m false) (f558c 22) (f559m false) (f559c 22) (f560m false) (f560c 22) (f561m false) (f561c 22) (f562m true) (f562c (- 9)) (f563m false) (f563c 0) (f564m true) (f564c 7) (f565m false) (f565c 0) (f566m false) (f566c 22) (f567m false) (f567c 22) (f568m false) (f568c 22) (f569m false) (f569c 22) (f570m true) (f570c 7) (f571m false) (f571c 0) (f572m true) (f572c 71) (f573m false) (f573c 0) (f574m false) (f574c 22) (f575m false) (f575c 22) (f576m false) (f576c 22) (f577m false) (f577c 22) (f578m true) (f578c 29) (f579m false) (f579c (- 21)) (f580m true) (f580c 7) (f581m false) (f581c 0) (f582m false) (f582c 1) (f583m false) (f583c 22) (f584m false) (f584c 1) (f585m false) (f585c 22) (f586m true) (f586c (- 35)) (f587m false) (f587c (- 42)) (f588m true) (f588c (- 51)) (f589m false) (f589c (- 21)) (f590m false) (f590c (- 20)) (f591m false) (f591c 1) (f592m false) (f592c 0) (f593m false) (f593c 13) (f594m true) (f594c (- 51)) (f595m false) (f595c (- 21)) (f596m true) (f596c 7) (f597m false) (f597c (- 21)) (f598m false) (f598c 13) (f599m false) (f599c 13) (f600m false) (f600c 20) (f601m false) (f601c 22) (f602m true) (f602c (- 35)) (f603m false) (f603c (- 42)) (f604m true) (f604c (- 51)) (f605m false) (f605c (- 21)) (f606m false) (f606c (- 1)) (f607m false) (f607c 20) (f608m false) (f608c 0) (f609m false) (f609c 20) (f610m true) (f610c (- 51)) (f611m false) (f611c (- 21)) (f612m true) (f612c (- 28)) (f613m false) (f613c (- 21)) (f614m false) (f614c 20) (f615m false) (f615c 20) (f616m false) (f616c 20) (f617m false) (f617c 22))