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