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