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