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