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