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