sat ((f0m true) (f0c (- 12574)) (f1m true) (f1c (- 5849)) (f2m true) (f2c 0) (f3m true) (f3c (- 14811)) (f4m true) (f4c (- 8089)) (f5m true) (f5c 12472) (f6m true) (f6c (- 10286)) (f7m true) (f7c 0) (f8m true) (f8c 602) (f9m false) (f9c 2) (f10m true) (f10c (- 14810)) (f11m true) (f11c 0) (f12m true) (f12c 47) (f13m true) (f13c 7547) (f14m true) (f14c 14066) (f15m false) (f15c (- 6725)) (f16m true) (f16c 794) (f17m true) (f17c 8351) (f18m true) (f18c (- 14974)) (f19m false) (f19c (- 5745)) (f20m true) (f20c 2504) (f21m false) (f21c 1) (f22m false) (f22c (- 7498)) (f23m false) (f23c (- 13243)) (f24m false) (f24c (- 4222)) (f25m true) (f25c (- 6209)) (f26m true) (f26c (- 802)) (f27m true) (f27c (- 22816)) (f28m true) (f28c 0) (f29m true) (f29c (- 8402)) (f30m true) (f30c (- 15719)) (f31m true) (f31c (- 6544)) (f32m true) (f32c (- 694)) (f33m false) (f33c 0) (f34m true) (f34c (- 22818)) (f35m true) (f35c 1) (f36m true) (f36c 101) (f37m true) (f37c 12889) (f38m false) (f38c 12470) (f39m false) (f39c (- 6355)) (f40m true) (f40c 5386) (f41m true) (f41c 8438) (f42m true) (f42c (- 11382)) (f43m true) (f43c (- 1525)) (f44m true) (f44c 5006) (f45m false) (f45c 1) (f46m false) (f46c 0) (f47m false) (f47c (- 8249)) (f48m true) (f48c 92) (f49m true) (f49c 8339) (f50m true) (f50c 15898) (f51m true) (f51c (- 6676)) (f52m true) (f52c 2607) (f53m true) (f53c 10855) (f54m false) (f54c (- 12470)) (f55m true) (f55c (- 3240)) (f56m true) (f56c 5008) (f57m true) (f57c 49) (f58m false) (f58c (- 6724)) (f59m false) (f59c (- 13243)) (f60m false) (f60c 1) (f61m false) (f61c (- 6724)) (f62m false) (f62c (- 13243)) (f63m true) (f63c (- 12523)) (f64m true) (f64c (- 3238)) (f65m true) (f65c 5008) (f66m true) (f66c (- 5327)) (f67m true) (f67c (- 6472)) (f68m true) (f68c 1087) (f69m true) (f69c (- 6678)) (f70m true) (f70c 2606) (f71m true) (f71c 5611) (f72m true) (f72c 2) (f73m true) (f73c (- 22816)) (f74m true) (f74c (- 10286)) (f75m false) (f75c 2) (f76m true) (f76c (- 22815)) (f77m true) (f77c 0) (f78m true) (f78c 199) (f79m true) (f79c 12992) (f80m true) (f80c 21327) (f81m true) (f81c (- 6196)) (f82m true) (f82c 6532) (f83m false) (f83c 6115) (f84m true) (f84c (- 14879)) (f85m true) (f85c (- 1025)) (f86m true) (f86c 9839) (f87m false) (f87c 4221) (f88m false) (f88c (- 6354)) (f89m true) (f89c (- 11381)) (f90m false) (f90c 4221) (f91m false) (f91c 0) (f92m false) (f92c (- 8249)) (f93m true) (f93c (- 816)) (f94m true) (f94c 13040) (f95m true) (f95c 23903) (f96m true) (f96c (- 6528)) (f97m true) (f97c 7326) (f98m true) (f98c 18190) (f99m true) (f99c (- 11939)) (f100m true) (f100c (- 1982)) (f101m false) (f101c 370) (f102m true) (f102c 4268) (f103m false) (f103c (- 2504)) (f104m false) (f104c (- 5745)) (f105m false) (f105c 1) (f106m false) (f106c (- 2504)) (f107m false) (f107c (- 5745)) (f108m true) (f108c (- 12739)) (f109m true) (f109c (- 2786)) (f110m true) (f110c 11981) (f111m true) (f111c (- 6528)) (f112m true) (f112c 7326) (f113m true) (f113c 1087) (f114m true) (f114c (- 13074)) (f115m true) (f115c (- 2677)) (f116m true) (f116c 5610) (f117m false) (f117c (- 4221)) (f118m true) (f118c (- 22815)) (f119m true) (f119c (- 6437)) (f120m false) (f120c 0) (f121m true) (f121c (- 22815)) (f122m true) (f122c (- 1154)) (f123m true) (f123c 96) (f124m true) (f124c 21724) (f125m true) (f125c 15898) (f126m true) (f126c (- 5933)) (f127m true) (f127c 15001) (f128m true) (f128c 10855) (f129m false) (f129c (- 12470)) (f130m true) (f130c (- 4951)) (f131m true) (f131c 5008) (f132m true) (f132c 1) (f133m false) (f133c (- 6724)) (f134m false) (f134c (- 13243)) (f135m false) (f135c 1) (f136m false) (f136c (- 6724)) (f137m false) (f137c (- 13243)) (f138m true) (f138c (- 12468)) (f139m true) (f139c 9152) (f140m true) (f140c 5008) (f141m true) (f141c (- 14715)) (f142m true) (f142c 6913) (f143m true) (f143c 1087) (f144m true) (f144c (- 1071)) (f145m true) (f145c 11436) (f146m true) (f146c 5610) (f147m true) (f147c 2) (f148m true) (f148c (- 14814)) (f149m true) (f149c (- 12642)) (f150m false) (f150c 2) (f151m true) (f151c 0) (f152m true) (f152c 0) (f153m true) (f153c 200) (f154m true) (f154c 4926) (f155m true) (f155c 21327) (f156m true) (f156c (- 6256)) (f157m true) (f157c 6913) (f158m false) (f158c 6115) (f159m true) (f159c (- 11283)) (f160m true) (f160c 1507) (f161m true) (f161c 6913) (f162m false) (f162c 4221) (f163m false) (f163c (- 6354)) (f164m true) (f164c (- 11381)) (f165m false) (f165c 4221) (f166m false) (f166c 0) (f167m false) (f167c (- 8249)) (f168m true) (f168c (- 12467)) (f169m true) (f169c 705) (f170m true) (f170c 5009) (f171m true) (f171c (- 14715)) (f172m true) (f172c 6913) (f173m true) (f173c (- 1489)) (f174m true) (f174c (- 12801)) (f175m true) (f175c 811) (f176m true) (f176c 5609) (f177m false) (f177c (- 1)) (f178m true) (f178c 0) (f179m true) (f179c (- 8945)) (f180m false) (f180c 0) (f181m true) (f181c 0) (f182m true) (f182c 1) (f183m true) (f183c 96) (f184m true) (f184c 8342) (f185m true) (f185c 17581) (f186m true) (f186c (- 6625)) (f187m true) (f187c 2606) (f188m true) (f188c 10855) (f189m false) (f189c (- 12470)) (f190m true) (f190c (- 3240)) (f191m true) (f191c 5007) (f192m true) (f192c 1) (f193m false) (f193c (- 6724)) (f194m false) (f194c (- 13243)) (f195m false) (f195c 1) (f196m false) (f196c (- 6724)) (f197m false) (f197c (- 13243)) (f198m true) (f198c (- 12476)) (f199m true) (f199c (- 3238)) (f200m true) (f200c 5007) (f201m true) (f201c (- 14715)) (f202m true) (f202c (- 6469)) (f203m true) (f203c 2770) (f204m true) (f204c (- 11867)) (f205m true) (f205c 2605) (f206m true) (f206c 2186) (f207m true) (f207c 2) (f208m true) (f208c (- 14811)) (f209m true) (f209c (- 10284)) (f210m false) (f210c 2) (f211m true) (f211c (- 14810)) (f212m true) (f212c 1) (f213m true) (f213c (- 12475)) (f214m true) (f214c (- 1525)) (f215m true) (f215c 5006) (f216m true) (f216c (- 14710)) (f217m true) (f217c (- 1922)) (f218m true) (f218c 17480) (f219m true) (f219c (- 11868)) (f220m true) (f220c 2604) (f221m true) (f221c 2185) (f222m true) (f222c 2) (f223m true) (f223c (- 14810)) (f224m true) (f224c 2) (f225m false) (f225c 2) (f226m true) (f226c (- 14810)) (f227m true) (f227c 0) (f228m true) (f228c 824) (f229m true) (f229c 8319) (f230m true) (f230c 16570) (f231m true) (f231c (- 6620)) (f232m true) (f232c 1590) (f233m true) (f233c 10855) (f234m false) (f234c (- 12470)) (f235m true) (f235c (- 3240)) (f236m true) (f236c 3998) (f237m true) (f237c 1) (f238m false) (f238c (- 6724)) (f239m false) (f239c (- 13243)) (f240m false) (f240c 1) (f241m false) (f241c (- 6724)) (f242m false) (f242c (- 13243)) (f243m true) (f243c (- 11748)) (f244m true) (f244c (- 4257)) (f245m true) (f245c 3998) (f246m true) (f246c (- 14811)) (f247m true) (f247c (- 6492)) (f248m true) (f248c 1759) (f249m true) (f249c (- 6621)) (f250m true) (f250c 1) (f251m true) (f251c 4601) (f252m true) (f252c (- 12573)) (f253m true) (f253c (- 14811)) (f254m true) (f254c 0) (f255m false) (f255c 2) (f256m true) (f256c (- 14810)) (f257m true) (f257c 0) (f258m true) (f258c 269) (f259m true) (f259c 17371) (f260m true) (f260c 19074) (f261m true) (f261c (- 5561)) (f262m true) (f262c 6826) (f263m false) (f263c 5745) (f264m false) (f264c (- 12100)) (f265m true) (f265c 979) (f266m true) (f266c 2691) (f267m true) (f267c 1) (f268m false) (f268c (- 6724)) (f269m false) (f269c (- 5745)) (f270m false) (f270c 1) (f271m false) (f271c (- 6724)) (f272m false) (f272c (- 5745)) (f273m false) (f273c 370) (f274m true) (f274c 19717) (f275m true) (f275c 22109) (f276m true) (f276c (- 6086)) (f277m true) (f277c 12214) (f278m true) (f278c 12721) (f279m true) (f279c (- 7092)) (f280m true) (f280c 5987) (f281m true) (f281c 7694) (f282m false) (f282c 6725) (f283m false) (f283c (- 6354)) (f284m true) (f284c (- 8249)) (f285m false) (f285c 6725) (f286m false) (f286c 0) (f287m false) (f287c (- 8249)) (f288m false) (f288c (- 3852)) (f289m true) (f289c 15497) (f290m true) (f290c 17888) (f291m true) (f291c (- 6086)) (f292m true) (f292c 12214) (f293m true) (f293c (- 707)) (f294m true) (f294c (- 7787)) (f295m true) (f295c 5671) (f296m true) (f296c 7001) (f297m false) (f297c 2503) (f298m true) (f298c 0) (f299m true) (f299c (- 6542)) (f300m false) (f300c 2503) (f301m true) (f301c 0) (f302m true) (f302c 1) (f303m true) (f303c 94) (f304m true) (f304c 8323) (f305m true) (f305c 14111) (f306m true) (f306c (- 6623)) (f307m true) (f307c 1586) (f308m true) (f308c 4882) (f309m false) (f309c (- 12470)) (f310m true) (f310c (- 3240)) (f311m true) (f311c 5008) (f312m true) (f312c 823) (f313m false) (f313c (- 6724)) (f314m false) (f314c (- 13243)) (f315m false) (f315c 1) (f316m false) (f316c (- 6724)) (f317m false) (f317c (- 13243)) (f318m true) (f318c 8725) (f319m true) (f319c 9111) (f320m true) (f320c 14104) (f321m true) (f321c 1998) (f322m true) (f322c 2382) (f323m true) (f323c 7384) (f324m true) (f324c (- 14880)) (f325m true) (f325c (- 4153)) (f326m true) (f326c (- 863)) (f327m true) (f327c 1) (f328m false) (f328c (- 6724)) (f329m false) (f329c (- 12469)) (f330m false) (f330c 1) (f331m false) (f331c (- 6724)) (f332m false) (f332c (- 12469)) (f333m true) (f333c (- 3851)) (f334m true) (f334c (- 3465)) (f335m true) (f335c 1528) (f336m true) (f336c (- 6086)) (f337m true) (f337c (- 5700)) (f338m true) (f338c (- 707)) (f339m true) (f339c (- 14279)) (f340m true) (f340c (- 3553)) (f341m true) (f341c (- 260)) (f342m true) (f342c 2) (f343m true) (f343c 1) (f344m true) (f344c 1) (f345m false) (f345c 2) (f346m true) (f346c 0) (f347m true) (f347c 0) (f348m true) (f348c 150) (f349m true) (f349c 12931) (f350m true) (f350c 19074) (f351m true) (f351c (- 3031)) (f352m true) (f352c 6166) (f353m false) (f353c 5745) (f354m false) (f354c (- 12100)) (f355m true) (f355c (- 361)) (f356m true) (f356c 7510) (f357m true) (f357c 0) (f358m false) (f358c (- 6724)) (f359m false) (f359c (- 5745)) (f360m false) (f360c 1) (f361m false) (f361c (- 6724)) (f362m false) (f362c (- 5745)) (f363m false) (f363c 370) (f364m true) (f364c 19057) (f365m true) (f365c 19980) (f366m true) (f366c 2355) (f367m true) (f367c 8077) (f368m true) (f368c 15948) (f369m true) (f369c (- 4554)) (f370m true) (f370c 4643) (f371m true) (f371c 12516) (f372m false) (f372c 6725) (f373m false) (f373c (- 6354)) (f374m true) (f374c (- 8249)) (f375m false) (f375c 6725) (f376m false) (f376c 0) (f377m false) (f377c (- 8249)) (f378m false) (f378c (- 3852)) (f379m true) (f379c 14836) (f380m true) (f380c 11716) (f381m true) (f381c 2356) (f382m true) (f382c 8077) (f383m true) (f383c 15948) (f384m true) (f384c (- 5249)) (f385m true) (f385c 3340) (f386m true) (f386c 11822) (f387m false) (f387c 2503) (f388m true) (f388c (- 16091)) (f389m true) (f389c (- 8944)) (f390m false) (f390c 2503) (f391m true) (f391c (- 16091)) (f392m true) (f392c 1) (f393m true) (f393c 15751) (f394m true) (f394c (- 1537)) (f395m true) (f395c 14111) (f396m true) (f396c (- 7065)) (f397m true) (f397c 2606) (f398m true) (f398c 7339) (f399m false) (f399c (- 12470)) (f400m true) (f400c (- 4953)) (f401m true) (f401c (- 908)) (f402m true) (f402c 823) (f403m false) (f403c (- 6724)) (f404m false) (f404c (- 13243)) (f405m false) (f405c 1) (f406m false) (f406c (- 6724)) (f407m false) (f407c (- 13243)) (f408m true) (f408c (- 13274)) (f409m true) (f409c (- 5759)) (f410m true) (f410c (- 1710)) (f411m true) (f411c (- 7065)) (f412m true) (f412c (- 13355)) (f413m true) (f413c 7340) (f414m true) (f414c (- 13610)) (f415m true) (f415c 3339) (f416m true) (f416c (- 1604)) (f417m false) (f417c (- 4221)) (f418m true) (f418c (- 22819)) (f419m true) (f419c (- 13937)) (f420m false) (f420c 0) (f421m true) (f421c (- 22818)) (f422m true) (f422c 0) (f423m true) (f423c 150) (f424m true) (f424c 12934) (f425m true) (f425c 19074) (f426m true) (f426c (- 3031)) (f427m true) (f427c 6826) (f428m false) (f428c 5745) (f429m false) (f429c (- 12100)) (f430m true) (f430c 979) (f431m true) (f431c 7510) (f432m true) (f432c 48) (f433m false) (f433c (- 6724)) (f434m false) (f434c (- 5745)) (f435m false) (f435c 1) (f436m false) (f436c (- 6724)) (f437m false) (f437c (- 5745)) (f438m false) (f438c 370) (f439m true) (f439c 19717) (f440m true) (f440c 19980) (f441m true) (f441c 2356) (f442m true) (f442c 12214) (f443m true) (f443c 15948) (f444m true) (f444c (- 4554)) (f445m true) (f445c 16297) (f446m true) (f446c 12517) (f447m false) (f447c 6725) (f448m false) (f448c (- 6354)) (f449m true) (f449c (- 8249)) (f450m false) (f450c 6725) (f451m false) (f451c 0) (f452m false) (f452c (- 8249)) (f453m false) (f453c (- 3852)) (f454m true) (f454c 15497) (f455m true) (f455c 9737) (f456m true) (f456c 2356) (f457m true) (f457c 12214) (f458m true) (f458c 15948) (f459m true) (f459c (- 5247)) (f460m true) (f460c 15604) (f461m true) (f461c 11825) (f462m false) (f462c 2503) (f463m true) (f463c 0) (f464m true) (f464c 1) (f465m false) (f465c 2503) (f466m true) (f466c 0) (f467m true) (f467c 2) (f468m true) (f468c (- 15778)) (f469m true) (f469c (- 6549)) (f470m true) (f470c 2142) (f471m true) (f471c (- 23376)) (f472m true) (f472c (- 14147)) (f473m true) (f473c 8351) (f474m true) (f474c (- 5248)) (f475m true) (f475c 0) (f476m true) (f476c 1808) (f477m false) (f477c (- 4221)) (f478m true) (f478c (- 22817)) (f479m true) (f479c (- 14043)) (f480m false) (f480c 0) (f481m true) (f481c (- 22818)) (f482m true) (f482c 1) (f483m true) (f483c 150) (f484m true) (f484c 12936) (f485m true) (f485c 19074) (f486m true) (f486c (- 3031)) (f487m true) (f487c 6164) (f488m false) (f488c 5745) (f489m false) (f489c (- 12100)) (f490m true) (f490c 979) (f491m true) (f491c 2693) (f492m true) (f492c 7547) (f493m false) (f493c (- 6724)) (f494m false) (f494c (- 5745)) (f495m false) (f495c 1) (f496m false) (f496c (- 6724)) (f497m false) (f497c (- 5745)) (f498m false) (f498c 370) (f499m true) (f499c 4973) (f500m true) (f500c 15163) (f501m true) (f501c (- 6205)) (f502m true) (f502c 6581) (f503m true) (f503c 11131) (f504m true) (f504c (- 3051)) (f505m true) (f505c 1554) (f506m true) (f506c 7699) (f507m false) (f507c 6725) (f508m false) (f508c (- 6354)) (f509m true) (f509c (- 8249)) (f510m false) (f510c 6725) (f511m false) (f511c 0) (f512m false) (f512c (- 8249)) (f513m false) (f513c (- 3852)) (f514m true) (f514c 752) (f515m true) (f515c 11797) (f516m true) (f516c (- 6205)) (f517m true) (f517c 0) (f518m true) (f518c 11131) (f519m true) (f519c (- 15718)) (f520m true) (f520c 39) (f521m true) (f521c 7005) (f522m false) (f522c 2503) (f523m true) (f523c 0) (f524m true) (f524c 1) (f525m false) (f525c 2503) (f526m true) (f526c 0) (f527m true) (f527c 1) (f528m true) (f528c 824) (f529m true) (f529c 11443) (f530m true) (f530c 20712) (f531m true) (f531c (- 5929)) (f532m true) (f532c 1586) (f533m true) (f533c 10855) (f534m false) (f534c (- 12470)) (f535m true) (f535c (- 4949)) (f536m true) (f536c 5008) (f537m true) (f537c 49) (f538m false) (f538c (- 6724)) (f539m false) (f539c (- 13243)) (f540m false) (f540c 1) (f541m false) (f541c (- 6724)) (f542m false) (f542c (- 13243)) (f543m false) (f543c 0) (f544m true) (f544c 14477) (f545m true) (f545c 23746) (f546m true) (f546c (- 4032)) (f547m true) (f547c 6973) (f548m true) (f548c 14359) (f549m true) (f549c (- 9380)) (f550m true) (f550c 59) (f551m true) (f551c 9330) (f552m false) (f552c (- 773)) (f553m false) (f553c (- 6354)) (f554m true) (f554c (- 8249)) (f555m false) (f555c 1) (f556m false) (f556c 0) (f557m false) (f557c (- 8249)) (f558m true) (f558c 6536) (f559m true) (f559c 12990) (f560m true) (f560c 21327) (f561m true) (f561c (- 2695)) (f562m true) (f562c 6911) (f563m false) (f563c 6115) (f564m true) (f564c (- 8466)) (f565m true) (f565c 392) (f566m true) (f566c 10010) (f567m false) (f567c 4221) (f568m false) (f568c (- 6354)) (f569m true) (f569c (- 11381)) (f570m false) (f570c 4221) (f571m false) (f571c 0) (f572m false) (f572c (- 8249)) (f573m true) (f573c 5597) (f574m true) (f574c 14456) (f575m true) (f575c 24074) (f576m true) (f576c (- 1903)) (f577m true) (f577c 6933) (f578m true) (f578c 14844) (f579m true) (f579c (- 8438)) (f580m true) (f580c (- 1984)) (f581m false) (f581c 370) (f582m true) (f582c 1) (f583m false) (f583c (- 2504)) (f584m false) (f584c (- 5745)) (f585m false) (f585c 1) (f586m false) (f586c (- 2504)) (f587m false) (f587c (- 5745)) (f588m true) (f588c 5642) (f589m true) (f589c 14478) (f590m true) (f590c 23970) (f591m true) (f591c (- 1130)) (f592m true) (f592c 7729) (f593m true) (f593c 15638) (f594m true) (f594c (- 9379)) (f595m true) (f595c 1186) (f596m true) (f596c 9100) (f597m true) (f597c 2) (f598m false) (f598c (- 6724)) (f599m false) (f599c (- 8249)) (f600m false) (f600c 1) (f601m false) (f601c (- 6724)) (f602m false) (f602c (- 8249)) (f603m true) (f603c 2686) (f604m true) (f604c 12938) (f605m true) (f605c 19074) (f606m true) (f606c (- 3031)) (f607m true) (f607c 6826) (f608m false) (f608c 5745) (f609m false) (f609c (- 12100)) (f610m true) (f610c (- 1853)) (f611m true) (f611c (- 2504)) (f612m true) (f612c 7547) (f613m false) (f613c (- 6724)) (f614m false) (f614c (- 5745)) (f615m false) (f615c 1) (f616m false) (f616c (- 6724)) (f617m false) (f617c (- 5745)) (f618m false) (f618c 370) (f619m true) (f619c 13039) (f620m true) (f620c 19177) (f621m true) (f621c (- 3662)) (f622m true) (f622c 6585) (f623m true) (f623c 12721) (f624m true) (f624c (- 4554)) (f625m true) (f625c 1556) (f626m true) (f626c 7690) (f627m false) (f627c 6725) (f628m false) (f628c (- 6354)) (f629m true) (f629c (- 8249)) (f630m false) (f630c 6725) (f631m false) (f631c 0) (f632m false) (f632c (- 8249)) (f633m true) (f633c 9512) (f634m true) (f634c 15623) (f635m true) (f635c 20270) (f636m false) (f636c (- 6355)) (f637m true) (f637c 2784) (f638m true) (f638c 7798) (f639m true) (f639c (- 9405)) (f640m true) (f640c 842) (f641m true) (f641c 10194) (f642m true) (f642c 1) (f643m false) (f643c 0) (f644m false) (f644c (- 5745)) (f645m false) (f645c 1) (f646m false) (f646c 0) (f647m false) (f647c (- 5745)) (f648m true) (f648c 820) (f649m true) (f649c 9093) (f650m true) (f650c 14111) (f651m true) (f651c (- 6623)) (f652m true) (f652c 1586) (f653m true) (f653c 6608) (f654m false) (f654c (- 12470)) (f655m true) (f655c (- 7427)) (f656m true) (f656c 5008) (f657m true) (f657c 49) (f658m false) (f658c (- 6724)) (f659m false) (f659c (- 13243)) (f660m false) (f660c 1) (f661m false) (f661c (- 6724)) (f662m false) (f662c (- 13243)) (f663m true) (f663c 2230) (f664m true) (f664c 9140) (f665m true) (f665c 14156) (f666m true) (f666c (- 4119)) (f667m true) (f667c 2368) (f668m true) (f668c 7384) (f669m true) (f669c (- 14156)) (f670m true) (f670c (- 4161)) (f671m true) (f671c (- 641)) (f672m true) (f672c 823) (f673m false) (f673c (- 6724)) (f674m false) (f674c (- 12469)) (f675m false) (f675c 1) (f676m false) (f676c (- 6724)) (f677m false) (f677c (- 12469)) (f678m true) (f678c 2331) (f679m true) (f679c 15257) (f680m true) (f680c 20271) (f681m true) (f681c (- 6354)) (f682m true) (f682c 2785) (f683m true) (f683c 7799) (f684m true) (f684c (- 9152)) (f685m true) (f685c 843) (f686m true) (f686c 10195) (f687m false) (f687c 1) (f688m false) (f688c (- 6354)) (f689m true) (f689c (- 11381)) (f690m false) (f690c 1) (f691m false) (f691c 0) (f692m false) (f692c (- 8249)))