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