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