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