sat ((f0m false) (f0c 2) (f1m false) (f1c (- 138)) (f2m false) (f2c 1) (f3m true) (f3c (- 505)) (f4m false) (f4c (- 1)) (f5m false) (f5c 2) (f6m false) (f6c 0) (f7m true) (f7c (- 163)) (f8m true) (f8c 482) (f9m true) (f9c (- 15)) (f10m true) (f10c 2) (f11m true) (f11c 503) (f12m false) (f12c 0) (f13m true) (f13c (- 491)) (f14m true) (f14c 491) (f15m false) (f15c 0) (f16m false) (f16c 2) (f17m true) (f17c 339) (f18m true) (f18c 0) (f19m true) (f19c (- 382)) (f20m true) (f20c 232) (f21m true) (f21c (- 337)) (f22m false) (f22c 2) (f23m false) (f23c 2) (f24m true) (f24c 118) (f25m true) (f25c (- 343)) (f26m true) (f26c 459) (f27m true) (f27c (- 25)) (f28m false) (f28c 0) (f29m true) (f29c 343) (f30m false) (f30c 0) (f31m true) (f31c (- 491)) (f32m true) (f32c 155) (f33m false) (f33c 0) (f34m false) (f34c 2) (f35m true) (f35c 342) (f36m false) (f36c 2) (f37m true) (f37c 341) (f38m false) (f38c 0) (f39m true) (f39c (- 161)) (f40m true) (f40c 140) (f41m true) (f41c (- 17)) (f42m false) (f42c 2) (f43m true) (f43c 326) (f44m false) (f44c 2) (f45m true) (f45c 326) (f46m false) (f46c 2) (f47m true) (f47c (- 157)) (f48m false) (f48c 1) (f49m true) (f49c (- 158)) (f50m false) (f50c 4) (f51m false) (f51c 3) (f52m false) (f52c 4) (f53m false) (f53c 3) (f54m false) (f54c 0) (f55m true) (f55c (- 163)) (f56m true) (f56c 465) (f57m true) (f57c (- 32)) (f58m true) (f58c 1) (f59m true) (f59c 488) (f60m true) (f60c 2) (f61m true) (f61c 488) (f62m true) (f62c 120) (f63m true) (f63c (- 377)) (f64m true) (f64c 461) (f65m true) (f65c (- 57)) (f66m true) (f66c 147) (f67m true) (f67c 461) (f68m false) (f68c 0) (f69m true) (f69c 461) (f70m true) (f70c 120) (f71m true) (f71c (- 261)) (f72m true) (f72c 434) (f73m true) (f73c (- 82)) (f74m true) (f74c 0) (f75m true) (f75c 436) (f76m false) (f76c 0) (f77m true) (f77c 491) (f78m true) (f78c 231) (f79m true) (f79c (- 260)) (f80m true) (f80c 613) (f81m true) (f81c 228) (f82m false) (f82c 0) (f83m true) (f83c 489) (f84m false) (f84c 2) (f85m true) (f85c 384) (f86m true) (f86c 231) (f87m true) (f87c (- 156)) (f88m true) (f88c (- 1)) (f89m true) (f89c (- 160)) (f90m true) (f90c 2) (f91m true) (f91c 3) (f92m false) (f92c 2) (f93m false) (f93c 2) (f94m false) (f94c 0) (f95m true) (f95c (- 491)) (f96m true) (f96c 491) (f97m false) (f97c 0) (f98m false) (f98c 2) (f99m true) (f99c 495) (f100m false) (f100c 2) (f101m true) (f101c 165) (f102m false) (f102c 0) (f103m true) (f103c (- 163)) (f104m true) (f104c 506) (f105m true) (f105c 345) (f106m false) (f106c 2) (f107m true) (f107c 142) (f108m false) (f108c 2) (f109m true) (f109c 142) (f110m false) (f110c 2) (f111m true) (f111c (- 161)) (f112m false) (f112c 1) (f113m true) (f113c (- 160)) (f114m false) (f114c 4) (f115m false) (f115c 3) (f116m false) (f116c 4) (f117m false) (f117c 3) (f118m false) (f118c 0) (f119m true) (f119c (- 492)) (f120m true) (f120c 136) (f121m true) (f121c (- 30)) (f122m true) (f122c 1) (f123m true) (f123c 490) (f124m true) (f124c 2) (f125m true) (f125c 504) (f126m true) (f126c 118) (f127m true) (f127c (- 373)) (f128m true) (f128c 112) (f129m true) (f129c 111) (f130m true) (f130c 161) (f131m true) (f131c 479) (f132m false) (f132c 0) (f133m true) (f133c 407) (f134m true) (f134c (- 231)) (f135m true) (f135c (- 232)) (f136m true) (f136c 577) (f137m true) (f137c 86) (f138m true) (f138c 0) (f139m true) (f139c 382) (f140m false) (f140c 0) (f141m true) (f141c 382) (f142m true) (f142c 195) (f143m true) (f143c (- 296)) (f144m true) (f144c 1) (f145m true) (f145c (- 251)) (f146m true) (f146c 0) (f147m true) (f147c 234) (f148m false) (f148c 2) (f149m false) (f149c 2) (f150m false) (f150c 0) (f151m true) (f151c (- 491)) (f152m true) (f152c 155) (f153m false) (f153c 0) (f154m false) (f154c 2) (f155m true) (f155c 518) (f156m false) (f156c 2) (f157m true) (f157c 518) (f158m false) (f158c 0) (f159m true) (f159c (- 161)) (f160m true) (f160c 140) (f161m true) (f161c 346) (f162m false) (f162c 2) (f163m true) (f163c 503) (f164m false) (f164c 2) (f165m true) (f165c 503) (f166m false) (f166c 2) (f167m true) (f167c 209) (f168m false) (f168c 1) (f169m true) (f169c (- 159)) (f170m false) (f170c 4) (f171m false) (f171c 3) (f172m false) (f172c 4) (f173m false) (f173c 3) (f174m false) (f174c 2) (f175m true) (f175c (- 162)) (f176m false) (f176c 1) (f177m true) (f177c (- 159)) (f178m true) (f178c 4) (f179m true) (f179c (- 2)) (f180m false) (f180c (- 1)) (f181m false) (f181c 2) (f182m true) (f182c 236) (f183m true) (f183c (- 368)) (f184m true) (f184c 646) (f185m true) (f185c (- 50)) (f186m true) (f186c 118) (f187m true) (f187c 320) (f188m false) (f188c 0) (f189m true) (f189c 321) (f190m true) (f190c 155) (f191m true) (f191c (- 368)) (f192m true) (f192c 724) (f193m true) (f193c 201) (f194m false) (f194c 0) (f195m true) (f195c 489) (f196m false) (f196c 2) (f197m true) (f197c 339) (f198m true) (f198c 157) (f199m true) (f199c (- 368)) (f200m true) (f200c 387) (f201m true) (f201c (- 136)) (f202m true) (f202c 2) (f203m true) (f203c 2) (f204m false) (f204c 2) (f205m false) (f205c 2) (f206m false) (f206c 0) (f207m true) (f207c (- 489)) (f208m true) (f208c 493) (f209m false) (f209c 0) (f210m false) (f210c 2) (f211m true) (f211c 341) (f212m false) (f212c 2) (f213m true) (f213c 340) (f214m false) (f214c 0) (f215m true) (f215c (- 491)) (f216m true) (f216c 491) (f217m false) (f217c 0) (f218m false) (f218c 2) (f219m true) (f219c 339) (f220m false) (f220c 2) (f221m true) (f221c 339) (f222m true) (f222c 0) (f223m true) (f223c (- 491)) (f224m true) (f224c 154) (f225m true) (f225c (- 257)) (f226m true) (f226c 2) (f227m true) (f227c 2) (f228m false) (f228c 2) (f229m false) (f229c 2) (f230m true) (f230c 236) (f231m true) (f231c (- 370)) (f232m true) (f232c 727) (f233m true) (f233c (- 50)) (f234m true) (f234c 0) (f235m true) (f235c 318) (f236m false) (f236c 0) (f237m true) (f237c 318) (f238m true) (f238c 236) (f239m true) (f239c (- 541)) (f240m true) (f240c 805) (f241m true) (f241c 81) (f242m false) (f242c 0) (f243m true) (f243c 340) (f244m false) (f244c 2) (f245m true) (f245c 339) (f246m true) (f246c 236) (f247m true) (f247c (- 379)) (f248m true) (f248c 468) (f249m true) (f249c (- 256)) (f250m true) (f250c 2) (f251m true) (f251c 2) (f252m false) (f252c 2) (f253m false) (f253c 2) (f254m false) (f254c 0) (f255m true) (f255c (- 491)) (f256m true) (f256c 491) (f257m false) (f257c 0) (f258m false) (f258c 2) (f259m true) (f259c 341) (f260m false) (f260c 2) (f261m true) (f261c 339) (f262m true) (f262c 109) (f263m true) (f263c (- 380)) (f264m true) (f264c 233) (f265m true) (f265c (- 258)) (f266m true) (f266c (- 45)) (f267m true) (f267c 2) (f268m false) (f268c 2) (f269m false) (f269c 2) (f270m true) (f270c 114) (f271m true) (f271c (- 227)) (f272m true) (f272c 605) (f273m true) (f273c (- 50)) (f274m true) (f274c (- 1)) (f275m true) (f275c 341) (f276m false) (f276c 0) (f277m true) (f277c 342) (f278m true) (f278c 114) (f279m true) (f279c (- 541)) (f280m true) (f280c 603) (f281m true) (f281c 28) (f282m false) (f282c 0) (f283m true) (f283c 489) (f284m false) (f284c 2) (f285m true) (f285c 339) (f286m true) (f286c 112) (f287m true) (f287c (- 541)) (f288m true) (f288c 346) (f289m true) (f289c (- 309)) (f290m true) (f290c 2) (f291m true) (f291c 2) (f292m false) (f292c 2) (f293m false) (f293c 2) (f294m true) (f294c 111) (f295m true) (f295c (- 542)) (f296m true) (f296c 346) (f297m true) (f297c (- 259)) (f298m true) (f298c (- 43)) (f299m true) (f299c 1) (f300m false) (f300c 2) (f301m false) (f301c 2) (f302m true) (f302c 236) (f303m true) (f303c (- 370)) (f304m true) (f304c 727) (f305m true) (f305c 119) (f306m true) (f306c (- 1)) (f307m true) (f307c 343) (f308m false) (f308c 0) (f309m true) (f309c 343) (f310m true) (f310c 236) (f311m true) (f311c (- 372)) (f312m true) (f312c 725) (f313m true) (f313c 123) (f314m false) (f314c 0) (f315m true) (f315c 345) (f316m false) (f316c 2) (f317m true) (f317c 339) (f318m true) (f318c 236) (f319m true) (f319c (- 372)) (f320m true) (f320c 470) (f321m true) (f321c (- 212)) (f322m true) (f322c 2) (f323m true) (f323c 2) (f324m false) (f324c 2) (f325m false) (f325c 2) (f326m false) (f326c 0) (f327m true) (f327c (- 163)) (f328m true) (f328c 482) (f329m true) (f329c (- 30)) (f330m true) (f330c (- 156)) (f331m true) (f331c 503) (f332m true) (f332c (- 155)) (f333m true) (f333c 504) (f334m false) (f334c 0) (f335m true) (f335c (- 240)) (f336m true) (f336c 382) (f337m true) (f337c 325) (f338m true) (f338c 2) (f339m true) (f339c 336) (f340m false) (f340c 2) (f341m true) (f341c 336) (f342m true) (f342c 2) (f343m true) (f343c (- 59)) (f344m true) (f344c 233) (f345m true) (f345c (- 10)) (f346m true) (f346c 2) (f347m true) (f347c 1) (f348m false) (f348c 2) (f349m false) (f349c 2) (f350m false) (f350c 0) (f351m true) (f351c (- 486)) (f352m true) (f352c 543) (f353m false) (f353c 0) (f354m false) (f354c 2) (f355m true) (f355c 491) (f356m false) (f356c 2) (f357m true) (f357c 338) (f358m true) (f358c 118) (f359m true) (f359c (- 345)) (f360m true) (f360c 459) (f361m true) (f361c (- 25)) (f362m true) (f362c 121) (f363m true) (f363c 311) (f364m false) (f364c 0) (f365m true) (f365c 310) (f366m true) (f366c 236) (f367m true) (f367c (- 368)) (f368m true) (f368c 434) (f369m true) (f369c 112) (f370m true) (f370c 118) (f371m true) (f371c 161) (f372m false) (f372c 0) (f373m true) (f373c 161) (f374m true) (f374c 234) (f375m true) (f375c (- 368)) (f376m true) (f376c 741) (f377m true) (f377c 495) (f378m false) (f378c 0) (f379m true) (f379c 144) (f380m false) (f380c 0) (f381m true) (f381c 504) (f382m true) (f382c 3) (f383m true) (f383c 357) (f384m true) (f384c 234) (f385m true) (f385c (- 10)) (f386m false) (f386c 2) (f387m false) (f387c 1) (f388m false) (f388c 2) (f389m false) (f389c 2) (f390m false) (f390c 0) (f391m true) (f391c (- 491)) (f392m true) (f392c 493) (f393m false) (f393c 0) (f394m false) (f394c 2) (f395m true) (f395c 491) (f396m false) (f396c 2) (f397m true) (f397c 338) (f398m false) (f398c 0) (f399m true) (f399c (- 165)) (f400m true) (f400c 480) (f401m true) (f401c (- 7)) (f402m false) (f402c 2) (f403m true) (f403c 321) (f404m false) (f404c 2) (f405m true) (f405c 320) (f406m false) (f406c 0) (f407m true) (f407c (- 167)) (f408m true) (f408c 734) (f409m true) (f409c (- 20)) (f410m false) (f410c 2) (f411m true) (f411c 307) (f412m false) (f412c 2) (f413m true) (f413c 504) (f414m false) (f414c 0) (f415m true) (f415c (- 163)) (f416m true) (f416c 467) (f417m true) (f417c 301) (f418m true) (f418c 1) (f419m true) (f419c 486) (f420m true) (f420c 2) (f421m true) (f421c 486) (f422m true) (f422c 124) (f423m true) (f423c (- 44)) (f424m true) (f424c 459) (f425m true) (f425c 276) (f426m true) (f426c 143) (f427m true) (f427c 461) (f428m false) (f428c 0) (f429m true) (f429c 461) (f430m true) (f430c 242) (f431m true) (f431c (- 69)) (f432m true) (f432c 583) (f433m true) (f433c 251) (f434m true) (f434c 118) (f435m true) (f435c 459) (f436m false) (f436c 0) (f437m true) (f437c 459) (f438m true) (f438c 242) (f439m true) (f439c (- 508)) (f440m true) (f440c 733) (f441m true) (f441c 249) (f442m false) (f442c 0) (f443m true) (f443c 493) (f444m false) (f444c 2) (f445m true) (f445c 339) (f446m true) (f446c 242) (f447m true) (f447c (- 166)) (f448m true) (f448c 734) (f449m true) (f449c (- 19)) (f450m false) (f450c 2) (f451m true) (f451c 493) (f452m false) (f452c 2) (f453m true) (f453c 493) (f454m true) (f454c (- 57)) (f455m true) (f455c (- 223)) (f456m true) (f456c 434) (f457m true) (f457c (- 50)) (f458m true) (f458c 0) (f459m true) (f459c 318) (f460m false) (f460c 0) (f461m true) (f461c 318) (f462m true) (f462c (- 57)) (f463m true) (f463c (- 217)) (f464m true) (f464c 434) (f465m true) (f465c 270) (f466m false) (f466c 0) (f467m true) (f467c 490) (f468m false) (f468c 2) (f469m true) (f469c 339) (f470m true) (f470c (- 57)) (f471m true) (f471c (- 217)) (f472m true) (f472c 435) (f473m true) (f473c 272) (f474m false) (f474c 2) (f475m true) (f475c 491) (f476m false) (f476c 2) (f477m true) (f477c 491) (f478m false) (f478c 0) (f479m true) (f479c (- 491)) (f480m true) (f480c 489) (f481m false) (f481c 0) (f482m false) (f482c 2) (f483m true) (f483c 491) (f484m false) (f484c 2) (f485m true) (f485c 339) (f486m false) (f486c 0) (f487m true) (f487c (- 491)) (f488m true) (f488c 492) (f489m false) (f489c 0) (f490m false) (f490c 2) (f491m true) (f491c 493) (f492m false) (f492c 2) (f493m true) (f493c 340) (f494m false) (f494c 0) (f495m true) (f495c (- 489)) (f496m true) (f496c 494) (f497m false) (f497c 0) (f498m false) (f498c 2) (f499m true) (f499c 339) (f500m false) (f500c 2) (f501m true) (f501c 340) (f502m true) (f502c 118) (f503m true) (f503c (- 345)) (f504m true) (f504c 459) (f505m true) (f505c 116) (f506m true) (f506c (- 1)) (f507m true) (f507c 340) (f508m false) (f508c 0) (f509m true) (f509c 341) (f510m true) (f510c 236) (f511m true) (f511c (- 227)) (f512m true) (f512c 434) (f513m true) (f513c 112) (f514m true) (f514c 0) (f515m true) (f515c 314) (f516m false) (f516c 0) (f517m true) (f517c 314) (f518m false) (f518c 0) (f519m true) (f519c (- 176)) (f520m true) (f520c 482) (f521m true) (f521c (- 85)) (f522m true) (f522c 2) (f523m true) (f523c 490) (f524m true) (f524c 2) (f525m true) (f525c 491) (f526m false) (f526c 0) (f527m true) (f527c (- 574)) (f528m true) (f528c 1041) (f529m true) (f529c (- 79)) (f530m true) (f530c 2) (f531m true) (f531c 339) (f532m false) (f532c 2) (f533m true) (f533c 339) (f534m false) (f534c 0) (f535m true) (f535c (- 572)) (f536m true) (f536c 1040) (f537m true) (f537c (- 81)) (f538m false) (f538c 2) (f539m true) (f539c 341) (f540m false) (f540c 2) (f541m true) (f541c 482) (f542m false) (f542c 0) (f543m true) (f543c (- 489)) (f544m true) (f544c 772) (f545m false) (f545c 0) (f546m false) (f546c 2) (f547m true) (f547c 339) (f548m false) (f548c 2) (f549m true) (f549c 339) (f550m true) (f550c 118) (f551m true) (f551c (- 341)) (f552m true) (f552c 745) (f553m true) (f553c (- 27)) (f554m true) (f554c 0) (f555m true) (f555c 314) (f556m false) (f556c 0) (f557m true) (f557c 484) (f558m true) (f558c 236) (f559m true) (f559c (- 221)) (f560m true) (f560c 720) (f561m true) (f561c (- 54)) (f562m true) (f562c 0) (f563m true) (f563c 459) (f564m false) (f564c 0) (f565m true) (f565c 459) (f566m true) (f566c 557) (f567m true) (f567c (- 219)) (f568m true) (f568c 718) (f569m true) (f569c 262) (f570m false) (f570c 0) (f571m true) (f571c 444) (f572m false) (f572c 0) (f573m true) (f573c 497) (f574m true) (f574c 557) (f575m true) (f575c (- 221)) (f576m true) (f576c 1040) (f577m true) (f577c 264) (f578m false) (f578c 0) (f579m true) (f579c 482) (f580m false) (f580c 0) (f581m true) (f581c 482))