sat ((f0c 0) (f0m false) (f100c 6) (f100m true) (f101c 7) (f101m true) (f102c 3) (f102m false) (f103c 0) (f103m true) (f104c 0) (f104m true) (f105c 3) (f105m false) (f106c 7) (f106m true) (f107c 7) (f107m true) (f108c 2) (f108m false) (f109c 4) (f109m false) (f10c 7) (f10m true) (f110c 0) (f110m false) (f111c 0) (f111m false) (f112c 2) (f112m false) (f113c 2) (f113m true) (f114c 2) (f114m true) (f115c 0) (f115m false) (f116c 2) (f116m false) (f117c 3) (f117m false) (f118c 1) (f118m false) (f119c 1) (f119m false) (f11c 0) (f11m true) (f120c 3) (f120m false) (f121c 1) (f121m false) (f122c 1) (f122m false) (f123c 2) (f123m false) (f124c 4) (f124m false) (f125c 0) (f125m false) (f126c 0) (f126m true) (f127c 0) (f127m true) (f128c 0) (f128m true) (f129c 0) (f129m true) (f12c 2) (f12m false) (f130c 0) (f130m true) (f131c 0) (f131m true) (f132c 3) (f132m false) (f133c 5) (f133m true) (f134c 7) (f134m true) (f135c 3) (f135m false) (f136c 0) (f136m true) (f137c 0) (f137m true) (f138c 2) (f138m true) (f139c 0) (f139m false) (f13c 0) (f13m true) (f140c 2) (f140m false) (f141c 2) (f141m true) (f142c 7) (f142m true) (f143c 7) (f143m true) (f144c 7) (f144m true) (f145c 6) (f145m true) (f146c 7) (f146m true) (f147c 1) (f147m false) (f148c 6) (f148m true) (f149c 1) (f149m true) (f14c 0) (f14m false) (f150c 2) (f150m false) (f151c 6) (f151m true) (f152c 7) (f152m true) (f153c 0) (f153m false) (f154c 2) (f154m false) (f155c 3) (f155m true) (f156c 0) (f156m true) (f157c 0) (f157m false) (f158c 4) (f158m true) (f159c 2) (f159m false) (f15c 0) (f15m false) (f160c 4) (f160m false) (f161c 0) (f161m false) (f162c 5) (f162m true) (f163c 1) (f163m true) (f164c 3) (f164m false) (f165c 1) (f165m false) (f166c 1) (f166m true) (f167c 3) (f167m false) (f168c 2) (f168m true) (f169c 0) (f169m false) (f16c 2) (f16m false) (f170c 0) (f170m true) (f171c 0) (f171m true) (f172c 2) (f172m true) (f173c 0) (f173m true) (f174c 7) (f174m true) (f175c 7) (f175m true) (f176c 0) (f176m true) (f177c 6) (f177m true) (f178c 4) (f178m true) (f179c 6) (f179m true) (f17c 0) (f17m true) (f180c 1) (f180m false) (f181c 1) (f181m true) (f182c 0) (f182m true) (f183c 2) (f183m true) (f184c 0) (f184m false) (f185c 2) (f185m false) (f186c 0) (f186m true) (f187c 7) (f187m true) (f188c 0) (f188m true) (f189c 7) (f189m true) (f18c 2) (f18m true) (f190c 7) (f190m true) (f191c 0) (f191m true) (f192c 1) (f192m false) (f193c 7) (f193m true) (f194c 0) (f194m true) (f195c 2) (f195m false) (f196c 0) (f196m true) (f197c 7) (f197m true) (f198c 4) (f198m false) (f199c 0) (f199m false) (f19c 0) (f19m false) (f1c 1) (f1m false) (f200c 2) (f200m false) (f201c 2) (f201m false) (f202c 4) (f202m false) (f203c 0) (f203m false) (f204c 0) (f204m false) (f205c 2) (f205m false) (f206c 2) (f206m true) (f207c 5) (f207m false) (f208c 3) (f208m false) (f209c 0) (f209m true) (f20c 0) (f20m true) (f210c 5) (f210m false) (f211c 3) (f211m false) (f212c 2) (f212m true) (f213c 2) (f213m false) (f214c 4) (f214m false) (f215c 0) (f215m false) (f216c 0) (f216m false) (f217c 2) (f217m false) (f218c 3) (f218m true) (f219c 4) (f219m false) (f21c 3) (f21m false) (f220c 6) (f220m false) (f221c 2) (f221m false) (f222c 3) (f222m false) (f223c 1) (f223m true) (f224c 5) (f224m false) (f225c 3) (f225m false) (f226c 1) (f226m true) (f227c 5) (f227m false) (f228c 4) (f228m false) (f229c 0) (f229m false) (f22c 5) (f22m true) (f230c 2) (f230m false) (f231c 2) (f231m false) (f232c 4) (f232m false) (f233c 0) (f233m false) (f234c 0) (f234m false) (f235c 2) (f235m false) (f236c 1) (f236m true) (f237c 5) (f237m false) (f238c 3) (f238m false) (f239c 6) (f239m true) (f23c 1) (f23m true) (f240c 5) (f240m false) (f241c 3) (f241m false) (f242c 6) (f242m true) (f243c 6) (f243m false) (f244c 2) (f244m false) (f245c 4) (f245m false) (f246c 4) (f246m false) (f247c 6) (f247m false) (f248c 2) (f248m false) (f249c 2) (f249m false) (f24c 2) (f24m true) (f250c 4) (f250m false) (f251c 0) (f251m false) (f252c 7) (f252m false) (f253c 5) (f253m false) (f254c 3) (f254m false) (f255c 7) (f255m false) (f256c 5) (f256m false) (f257c 3) (f257m false) (f258c 2) (f258m false) (f259c 4) (f259m false) (f25c 0) (f25m false) (f260c 0) (f260m false) (f261c 0) (f261m false) (f262c 2) (f262m false) (f263c 2) (f263m true) (f264c 3) (f264m true) (f265c 0) (f265m false) (f266c 2) (f266m false) (f267c 3) (f267m false) (f268c 1) (f268m false) (f269c 1) (f269m false) (f26c 0) (f26m true) (f270c 3) (f270m false) (f271c 1) (f271m false) (f272c 1) (f272m false) (f273c 0) (f273m false) (f274c 2) (f274m false) (f275c 4) (f275m false) (f276c 5) (f276m true) (f277c 0) (f277m false) (f278c 2) (f278m false) (f279c 2) (f279m false) (f27c 0) (f27m true) (f280c 4) (f280m false) (f281c 0) (f281m false) (f282c 3) (f282m false) (f283c 1) (f283m false) (f284c 3) (f284m false) (f285c 3) (f285m false) (f286c 1) (f286m false) (f287c 3) (f287m false) (f288c 2) (f288m false) (f289c 4) (f289m false) (f28c 0) (f28m true) (f290c 0) (f290m false) (f291c 0) (f291m false) (f292c 2) (f292m false) (f293c 2) (f293m true) (f294c 4) (f294m true) (f295c 0) (f295m false) (f296c 2) (f296m false) (f297c 3) (f297m false) (f298c 1) (f298m false) (f299c 1) (f299m false) (f29c 0) (f29m true) (f2c 2) (f2m true) (f300c 3) (f300m false) (f301c 1) (f301m false) (f302c 1) (f302m false) (f303c 0) (f303m false) (f304c 2) (f304m false) (f305c 2) (f305m true) (f306c 3) (f306m true) (f307c 0) (f307m false) (f308c 4) (f308m true) (f309c 2) (f309m false) (f30c 0) (f30m true) (f310c 4) (f310m false) (f311c 0) (f311m false) (f312c 3) (f312m true) (f313c 1) (f313m true) (f314c 3) (f314m false) (f315c 1) (f315m false) (f316c 1) (f316m true) (f317c 3) (f317m false) (f318c 2) (f318m false) (f319c 4) (f319m false) (f31c 0) (f31m true) (f320c 0) (f320m false) (f321c 0) (f321m false) (f322c 2) (f322m false) (f323c 2) (f323m true) (f324c 4) (f324m true) (f325c 0) (f325m false) (f326c 2) (f326m true) (f327c 3) (f327m false) (f328c 1) (f328m false) (f329c 1) (f329m true) (f32c 0) (f32m true) (f330c 3) (f330m false) (f331c 1) (f331m false) (f332c 1) (f332m true) (f33c 1) (f33m false) (f34c 0) (f34m true) (f35c 0) (f35m true) (f36c 1) (f36m true) (f37c 0) (f37m false) (f38c 2) (f38m false) (f39c 1) (f39m true) (f3c 0) (f3m true) (f40c 0) (f40m true) (f41c 0) (f41m false) (f42c 0) (f42m false) (f43c 2) (f43m false) (f44c 1) (f44m true) (f45c 1) (f45m false) (f46c 1) (f46m true) (f47c 1) (f47m false) (f48c 4) (f48m false) (f49c 0) (f49m false) (f4c 0) (f4m true) (f50c 2) (f50m false) (f51c 2) (f51m false) (f52c 4) (f52m false) (f53c 0) (f53m false) (f54c 0) (f54m false) (f55c 2) (f55m false) (f56c 1) (f56m true) (f57c 5) (f57m false) (f58c 3) (f58m false) (f59c 0) (f59m true) (f5c 0) (f5m true) (f60c 5) (f60m false) (f61c 3) (f61m false) (f62c 1) (f62m true) (f63c 4) (f63m false) (f64c 5) (f64m false) (f65c 2) (f65m false) (f66c 5) (f66m true) (f67c 7) (f67m true) (f68c 7) (f68m true) (f69c 6) (f69m true) (f6c 0) (f6m true) (f70c 6) (f70m true) (f71c 7) (f71m true) (f72c 5) (f72m false) (f73c 1) (f73m true) (f74c 0) (f74m true) (f75c 5) (f75m false) (f76c 6) (f76m true) (f77c 6) (f77m true) (f78c 4) (f78m false) (f79c 0) (f79m false) (f7c 0) (f7m true) (f80c 2) (f80m false) (f81c 2) (f81m false) (f82c 4) (f82m false) (f83c 0) (f83m false) (f84c 0) (f84m false) (f85c 2) (f85m false) (f86c 2) (f86m true) (f87c 5) (f87m false) (f88c 3) (f88m false) (f89c 5) (f89m true) (f8c 0) (f8m true) (f90c 5) (f90m false) (f91c 3) (f91m false) (f92c 1) (f92m true) (f93c 2) (f93m false) (f94c 4) (f94m false) (f95c 0) (f95m false) (f96c 0) (f96m true) (f97c 7) (f97m true) (f98c 7) (f98m true) (f99c 7) (f99m true) (f9c 2) (f9m false) (l0c 4) (l0m false) (l100c 6) (l100m true) (l101c 6) (l101m true) (l102c 4) (l102m false) (l103c 3) (l103m true) (l104c 4) (l104m true) (l105c 4) (l105m false) (l106c 0) (l106m true) (l107c 0) (l107m true) (l108c 0) (l108m false) (l109c 0) (l109m false) (l10c 3) (l10m true) (l110c 2) (l110m false) (l111c 2) (l111m true) (l112c 2) (l112m true) (l113c 2) (l113m false) (l114c 2) (l114m false) (l115c 2) (l115m false) (l116c 4) (l116m true) (l117c 2) (l117m false) (l118c 4) (l118m true) (l119c 4) (l119m false) (l11c 2) (l11m false) (l120c 1) (l120m true) (l121c 4) (l121m false) (l122c 0) (l122m false) (l123c 2) (l123m true) (l124c 0) (l124m true) (l125c 0) (l125m false) (l126c 3) (l126m true) (l127c 0) (l127m false) (l128c 4) (l128m true) (l129c 0) (l129m false) (l12c 2) (l12m false) (l130c 2) (l130m true) (l131c 2) (l131m false) (l132c 2) (l132m true) (l133c 2) (l133m false) (l134c 2) (l134m true) (l135c 1) (l135m true) (l136c 2) (l136m true) (l137c 2) (l137m true) (l138c 5) (l138m false) (l139c 6) (l139m true) (l13c 2) (l13m false) (l140c 5) (l140m true) (l141c 5) (l141m false) (l142c 3) (l142m false) (l143c 6) (l143m true) (l144c 5) (l144m true) (l145c 3) (l145m false) (l146c 5) (l146m true) (l147c 5) (l147m true) (l148c 5) (l148m true) (l149c 5) (l149m true) (l14c 2) (l14m true) (l150c 5) (l150m false) (l151c 3) (l151m false) (l152c 1) (l152m true) (l153c 2) (l153m true) (l154c 2) (l154m false) (l155c 4) (l155m true) (l156c 2) (l156m false) (l157c 2) (l157m true) (l158c 4) (l158m false) (l159c 2) (l159m true) (l15c 2) (l15m false) (l160c 4) (l160m false) (l161c 0) (l161m true) (l162c 0) (l162m false) (l163c 0) (l163m true) (l164c 0) (l164m false) (l165c 0) (l165m true) (l166c 3) (l166m true) (l167c 7) (l167m true) (l168c 0) (l168m true) (l169c 0) (l169m true) (l16c 3) (l16m true) (l170c 0) (l170m true) (l171c 0) (l171m true) (l172c 7) (l172m true) (l173c 0) (l173m true) (l174c 0) (l174m true) (l175c 0) (l175m true) (l176c 7) (l176m true) (l177c 0) (l177m true) (l178c 0) (l178m true) (l179c 0) (l179m true) (l17c 4) (l17m false) (l180c 7) (l180m true) (l181c 0) (l181m true) (l182c 0) (l182m true) (l183c 0) (l183m true) (l184c 6) (l184m true) (l185c 0) (l185m true) (l186c 0) (l186m true) (l187c 0) (l187m true) (l188c 7) (l188m true) (l189c 6) (l189m true) (l18c 1) (l18m true) (l190c 3) (l190m false) (l191c 2) (l191m true) (l192c 3) (l192m false) (l193c 7) (l193m true) (l194c 2) (l194m true) (l195c 7) (l195m true) (l196c 0) (l196m true) (l197c 1) (l197m true) (l198c 0) (l198m true) (l199c 6) (l199m true) (l19c 4) (l19m false) (l1c 4) (l1m true) (l200c 0) (l200m true) (l201c 3) (l201m false) (l202c 7) (l202m true) (l203c 7) (l203m true) (l204c 4) (l204m true) (l205c 1) (l205m true) (l206c 2) (l206m false) (l207c 2) (l207m false) (l208c 2) (l208m true) (l209c 1) (l209m true) (l20c 0) (l20m false) (l210c 4) (l210m false) (l211c 4) (l211m false) (l212c 1) (l212m true) (l213c 0) (l213m false) (l214c 0) (l214m true) (l215c 0) (l215m false) (l216c 1) (l216m true) (l217c 2) (l217m true) (l218c 0) (l218m false) (l219c 0) (l219m false) (l21c 0) (l21m true) (l220c 1) (l220m true) (l221c 2) (l221m true) (l222c 2) (l222m false) (l223c 2) (l223m false) (l224c 2) (l224m true) (l225c 1) (l225m true) (l226c 2) (l226m true) (l227c 2) (l227m true) (l228c 1) (l228m true) (l229c 2) (l229m true) (l22c 2) (l22m true) (l230c 3) (l230m true) (l231c 2) (l231m true) (l232c 0) (l232m false) (l233c 2) (l233m true) (l234c 2) (l234m true) (l235c 0) (l235m false) (l236c 2) (l236m false) (l237c 2) (l237m false) (l238c 2) (l238m true) (l239c 2) (l239m false) (l23c 0) (l23m false) (l240c 5) (l240m true) (l241c 1) (l241m true) (l242c 3) (l242m false) (l243c 3) (l243m false) (l244c 3) (l244m true) (l245c 0) (l245m true) (l246c 1) (l246m false) (l247c 1) (l247m false) (l248c 1) (l248m false) (l249c 1) (l249m true) (l24c 3) (l24m true) (l250c 1) (l250m true) (l251c 1) (l251m false) (l252c 3) (l252m false) (l253c 1) (l253m false) (l254c 1) (l254m false) (l255c 2) (l255m false) (l256c 1) (l256m false) (l257c 6) (l257m true) (l258c 2) (l258m false) (l259c 4) (l259m false) (l25c 0) (l25m false) (l260c 3) (l260m false) (l261c 2) (l261m true) (l262c 4) (l262m false) (l263c 0) (l263m false) (l264c 5) (l264m true) (l265c 1) (l265m true) (l266c 0) (l266m false) (l267c 0) (l267m true) (l268c 5) (l268m true) (l269c 7) (l269m true) (l26c 2) (l26m true) (l270c 0) (l270m true) (l271c 7) (l271m true) (l272c 4) (l272m true) (l273c 1) (l273m true) (l274c 0) (l274m true) (l275c 6) (l275m true) (l276c 1) (l276m true) (l277c 6) (l277m true) (l278c 0) (l278m true) (l279c 6) (l279m true) (l27c 0) (l27m false) (l280c 3) (l280m true) (l281c 6) (l281m true) (l282c 0) (l282m true) (l283c 1) (l283m true) (l284c 7) (l284m true) (l285c 2) (l285m true) (l286c 0) (l286m true) (l287c 6) (l287m true) (l288c 5) (l288m true) (l289c 6) (l289m true) (l28c 3) (l28m true) (l290c 0) (l290m true) (l291c 3) (l291m false) (l292c 2) (l292m false) (l293c 6) (l293m true) (l294c 3) (l294m false) (l295c 0) (l295m true) (l296c 0) (l296m true) (l297c 0) (l297m true) (l298c 5) (l298m true) (l299c 0) (l299m true) (l29c 2) (l29m false) (l2c 4) (l2m true) (l300c 0) (l300m true) (l301c 0) (l301m true) (l302c 7) (l302m true) (l303c 3) (l303m false) (l304c 0) (l304m true) (l305c 0) (l305m true) (l306c 2) (l306m true) (l307c 2) (l307m true) (l308c 2) (l308m true) (l309c 2) (l309m true) (l30c 2) (l30m true) (l310c 0) (l310m false) (l311c 0) (l311m true) (l312c 0) (l312m true) (l313c 0) (l313m false) (l314c 2) (l314m false) (l315c 1) (l315m false) (l316c 2) (l316m true) (l317c 2) (l317m false) (l318c 2) (l318m true) (l319c 7) (l319m true) (l31c 2) (l31m false) (l320c 0) (l320m true) (l321c 2) (l321m true) (l322c 0) (l322m true) (l323c 0) (l323m true) (l324c 0) (l324m true) (l325c 7) (l325m true) (l326c 0) (l326m true) (l327c 0) (l327m true) (l328c 0) (l328m true) (l329c 7) (l329m true) (l32c 4) (l32m true) (l330c 0) (l330m true) (l331c 0) (l331m true) (l332c 0) (l332m true) (l333c 7) (l333m true) (l334c 0) (l334m true) (l335c 0) (l335m true) (l336c 0) (l336m true) (l337c 6) (l337m true) (l338c 0) (l338m true) (l339c 0) (l339m true) (l33c 1) (l33m true) (l340c 0) (l340m true) (l341c 7) (l341m true) (l342c 1) (l342m false) (l343c 5) (l343m true) (l344c 6) (l344m true) (l345c 1) (l345m false) (l346c 0) (l346m true) (l347c 1) (l347m true) (l348c 0) (l348m true) (l349c 6) (l349m true) (l34c 1) (l34m true) (l350c 0) (l350m true) (l351c 0) (l351m true) (l352c 2) (l352m true) (l353c 1) (l353m true) (l354c 2) (l354m false) (l355c 6) (l355m true) (l356c 7) (l356m true) (l357c 0) (l357m true) (l358c 0) (l358m false) (l359c 1) (l359m true) (l35c 1) (l35m true) (l360c 0) (l360m false) (l361c 2) (l361m true) (l362c 2) (l362m false) (l363c 2) (l363m false) (l364c 2) (l364m false) (l365c 3) (l365m true) (l366c 3) (l366m true) (l367c 2) (l367m true) (l368c 3) (l368m true) (l369c 0) (l369m true) (l36c 5) (l36m false) (l370c 0) (l370m true) (l371c 1) (l371m true) (l372c 0) (l372m true) (l373c 1) (l373m true) (l374c 2) (l374m true) (l375c 0) (l375m false) (l376c 0) (l376m false) (l377c 4) (l377m true) (l378c 0) (l378m true) (l379c 2) (l379m true) (l37c 6) (l37m true) (l380c 4) (l380m true) (l381c 2) (l381m false) (l382c 2) (l382m false) (l383c 3) (l383m true) (l384c 2) (l384m false) (l385c 0) (l385m true) (l386c 4) (l386m false) (l387c 1) (l387m true) (l388c 4) (l388m false) (l389c 0) (l389m false) (l38c 2) (l38m true) (l390c 0) (l390m true) (l391c 2) (l391m true) (l392c 0) (l392m false) (l393c 3) (l393m true) (l394c 5) (l394m true) (l395c 5) (l395m true) (l396c 5) (l396m true) (l397c 1) (l397m true) (l398c 2) (l398m true) (l399c 2) (l399m true) (l39c 5) (l39m false) (l3c 4) (l3m false) (l400c 1) (l400m true) (l401c 3) (l401m false) (l402c 2) (l402m true) (l403c 5) (l403m true) (l404c 3) (l404m false) (l405c 1) (l405m false) (l406c 1) (l406m true) (l407c 3) (l407m false) (l408c 2) (l408m true) (l409c 5) (l409m true) (l40c 3) (l40m false) (l410c 2) (l410m true) (l411c 2) (l411m true) (l412c 4) (l412m true) (l413c 0) (l413m false) (l414c 4) (l414m true) (l415c 0) (l415m false) (l416c 4) (l416m true) (l417c 3) (l417m true) (l418c 0) (l418m true) (l419c 0) (l419m true) (l41c 3) (l41m true) (l420c 0) (l420m true) (l421c 5) (l421m true) (l422c 2) (l422m true) (l423c 0) (l423m true) (l424c 0) (l424m true) (l425c 0) (l425m true) (l426c 0) (l426m true) (l427c 2) (l427m true) (l428c 1) (l428m true) (l429c 2) (l429m true) (l42c 5) (l42m true) (l430c 0) (l430m true) (l431c 0) (l431m true) (l432c 0) (l432m true) (l433c 0) (l433m true) (l434c 0) (l434m true) (l435c 7) (l435m true) (l436c 0) (l436m true) (l437c 0) (l437m true) (l438c 0) (l438m true) (l439c 7) (l439m true) (l43c 3) (l43m false) (l440c 1) (l440m true) (l441c 6) (l441m true) (l442c 5) (l442m true) (l443c 0) (l443m true) (l444c 6) (l444m true) (l445c 6) (l445m true) (l446c 5) (l446m true) (l447c 6) (l447m true) (l448c 0) (l448m true) (l449c 0) (l449m true) (l44c 1) (l44m true) (l450c 0) (l450m true) (l451c 4) (l451m true) (l452c 0) (l452m true) (l453c 0) (l453m true) (l454c 0) (l454m true) (l455c 6) (l455m true) (l456c 1) (l456m false) (l457c 1) (l457m true) (l458c 0) (l458m true) (l459c 2) (l459m true) (l45c 0) (l45m true) (l460c 2) (l460m true) (l461c 2) (l461m true) (l462c 2) (l462m true) (l463c 0) (l463m false) (l464c 5) (l464m true) (l465c 4) (l465m true) (l466c 0) (l466m false) (l467c 2) (l467m false) (l468c 1) (l468m false) (l469c 2) (l469m true) (l46c 1) (l46m true) (l470c 2) (l470m false) (l471c 0) (l471m true) (l472c 0) (l472m true) (l473c 1) (l473m true) (l474c 0) (l474m true) (l475c 0) (l475m true) (l476c 0) (l476m true) (l477c 0) (l477m true) (l478c 7) (l478m true) (l479c 7) (l479m true) (l47c 0) (l47m true) (l480c 7) (l480m true) (l481c 4) (l481m true) (l482c 0) (l482m true) (l483c 0) (l483m true) (l484c 0) (l484m true) (l485c 0) (l485m true) (l486c 7) (l486m true) (l487c 0) (l487m true) (l488c 0) (l488m true) (l489c 0) (l489m true) (l48c 5) (l48m false) (l490c 7) (l490m true) (l491c 6) (l491m true) (l492c 7) (l492m true) (l493c 7) (l493m true) (l494c 0) (l494m true) (l495c 1) (l495m false) (l496c 5) (l496m true) (l497c 2) (l497m true) (l498c 1) (l498m false) (l499c 0) (l499m true) (l49c 3) (l49m false) (l4c 0) (l4m true) (l500c 0) (l500m true) (l501c 0) (l501m true) (l502c 7) (l502m true) (l503c 6) (l503m true) (l504c 7) (l504m true) (l505c 7) (l505m true) (l506c 0) (l506m true) (l507c 2) (l507m false) (l508c 0) (l508m true) (l509c 7) (l509m true) (l50c 1) (l50m true) (l510c 4) (l510m false) (l511c 3) (l511m true) (l512c 4) (l512m true) (l513c 4) (l513m false) (l514c 0) (l514m true) (l515c 3) (l515m true) (l516c 0) (l516m false) (l517c 0) (l517m false) (l518c 2) (l518m false) (l519c 2) (l519m true) (l51c 4) (l51m false) (l520c 2) (l520m true) (l521c 2) (l521m false) (l522c 2) (l522m false) (l523c 2) (l523m false) (l524c 3) (l524m true) (l525c 2) (l525m false) (l526c 3) (l526m true) (l527c 4) (l527m false) (l528c 1) (l528m true) (l529c 4) (l529m false) (l52c 3) (l52m false) (l530c 0) (l530m false) (l531c 0) (l531m true) (l532c 0) (l532m true) (l533c 0) (l533m false) (l534c 1) (l534m true) (l535c 0) (l535m false) (l536c 4) (l536m true) (l537c 0) (l537m false) (l538c 3) (l538m true) (l539c 2) (l539m false) (l53c 2) (l53m true) (l540c 2) (l540m true) (l541c 2) (l541m false) (l542c 4) (l542m true) (l543c 1) (l543m true) (l544c 2) (l544m true) (l545c 2) (l545m true) (l546c 5) (l546m false) (l547c 6) (l547m true) (l548c 2) (l548m true) (l549c 5) (l549m false) (l54c 4) (l54m false) (l550c 3) (l550m false) (l551c 3) (l551m true) (l552c 5) (l552m true) (l553c 3) (l553m false) (l554c 0) (l554m true) (l555c 0) (l555m true) (l556c 0) (l556m true) (l557c 0) (l557m true) (l558c 5) (l558m false) (l559c 3) (l559m false) (l55c 0) (l55m false) (l560c 2) (l560m true) (l561c 4) (l561m true) (l562c 2) (l562m false) (l563c 2) (l563m false) (l564c 2) (l564m false) (l565c 4) (l565m true) (l566c 4) (l566m false) (l567c 4) (l567m false) (l568c 4) (l568m false) (l569c 1) (l569m true) (l56c 5) (l56m false) (l570c 0) (l570m false) (l571c 3) (l571m true) (l572c 0) (l572m false) (l573c 3) (l573m true) (l574c 4) (l574m true) (l575c 0) (l575m false) (l576c 0) (l576m false) (l577c 3) (l577m true) (l578c 1) (l578m true) (l579c 2) (l579m false) (l57c 4) (l57m true) (l580c 2) (l580m false) (l581c 3) (l581m true) (l582c 2) (l582m true) (l583c 3) (l583m true) (l584c 3) (l584m true) (l585c 4) (l585m false) (l586c 4) (l586m false) (l587c 7) (l587m true) (l588c 4) (l588m false) (l589c 0) (l589m false) (l58c 5) (l58m false) (l590c 6) (l590m false) (l591c 3) (l591m true) (l592c 6) (l592m false) (l593c 2) (l593m false) (l594c 2) (l594m false) (l595c 3) (l595m true) (l596c 2) (l596m false) (l597c 4) (l597m true) (l598c 3) (l598m false) (l599c 3) (l599m true) (l59c 2) (l59m false) (l5c 0) (l5m true) (l600c 3) (l600m false) (l601c 3) (l601m true) (l602c 5) (l602m true) (l603c 2) (l603m true) (l604c 1) (l604m true) (l605c 5) (l605m false) (l606c 5) (l606m false) (l607c 5) (l607m true) (l608c 5) (l608m false) (l609c 3) (l609m false) (l60c 1) (l60m false) (l610c 1) (l610m true) (l611c 5) (l611m false) (l612c 4) (l612m false) (l613c 3) (l613m true) (l614c 4) (l614m true) (l615c 4) (l615m false) (l616c 0) (l616m true) (l617c 3) (l617m true) (l618c 0) (l618m false) (l619c 0) (l619m false) (l61c 2) (l61m true) (l620c 2) (l620m false) (l621c 2) (l621m true) (l622c 1) (l622m true) (l623c 2) (l623m false) (l624c 2) (l624m false) (l625c 2) (l625m false) (l626c 2) (l626m true) (l627c 2) (l627m false) (l628c 3) (l628m true) (l629c 4) (l629m false) (l62c 2) (l62m false) (l630c 1) (l630m true) (l631c 4) (l631m false) (l632c 0) (l632m false) (l633c 0) (l633m true) (l634c 2) (l634m true) (l635c 0) (l635m false) (l636c 3) (l636m true) (l637c 0) (l637m false) (l638c 1) (l638m true) (l639c 0) (l639m false) (l63c 2) (l63m true) (l640c 3) (l640m true) (l641c 2) (l641m false) (l642c 2) (l642m true) (l643c 2) (l643m false) (l644c 1) (l644m true) (l645c 1) (l645m true) (l646c 1) (l646m true) (l647c 1) (l647m true) (l648c 5) (l648m false) (l649c 6) (l649m true) (l64c 3) (l64m true) (l650c 2) (l650m true) (l651c 5) (l651m false) (l652c 3) (l652m false) (l653c 6) (l653m true) (l654c 3) (l654m true) (l655c 3) (l655m false) (l656c 3) (l656m true) (l657c 6) (l657m true) (l658c 6) (l658m true) (l659c 6) (l659m true) (l65c 0) (l65m true) (l660c 5) (l660m false) (l661c 3) (l661m false) (l662c 6) (l662m true) (l663c 6) (l663m false) (l664c 6) (l664m true) (l665c 0) (l665m false) (l666c 6) (l666m false) (l667c 2) (l667m false) (l668c 3) (l668m true) (l669c 2) (l669m false) (l66c 5) (l66m true) (l670c 2) (l670m false) (l671c 4) (l671m false) (l672c 3) (l672m true) (l673c 4) (l673m true) (l674c 4) (l674m false) (l675c 4) (l675m false) (l676c 4) (l676m false) (l677c 5) (l677m true) (l678c 4) (l678m false) (l679c 0) (l679m false) (l67c 0) (l67m true) (l680c 6) (l680m false) (l681c 3) (l681m true) (l682c 6) (l682m false) (l683c 2) (l683m false) (l684c 2) (l684m false) (l685c 2) (l685m true) (l686c 2) (l686m false) (l687c 2) (l687m true) (l688c 2) (l688m false) (l689c 2) (l689m true) (l68c 0) (l68m true) (l690c 2) (l690m false) (l691c 4) (l691m true) (l692c 4) (l692m false) (l693c 3) (l693m true) (l694c 4) (l694m false) (l695c 0) (l695m true) (l696c 0) (l696m false) (l697c 0) (l697m true) (l698c 0) (l698m false) (l699c 7) (l699m false) (l69c 0) (l69m true) (l6c 0) (l6m false) (l700c 7) (l700m true) (l701c 7) (l701m true) (l702c 7) (l702m false) (l703c 5) (l703m false) (l704c 5) (l704m false) (l705c 5) (l705m true) (l706c 5) (l706m false) (l707c 3) (l707m true) (l708c 3) (l708m false) (l709c 3) (l709m true) (l70c 7) (l70m true) (l710c 3) (l710m false) (l711c 7) (l711m false) (l712c 5) (l712m false) (l713c 3) (l713m false) (l714c 4) (l714m true) (l715c 1) (l715m true) (l716c 2) (l716m false) (l717c 2) (l717m false) (l718c 2) (l718m true) (l719c 1) (l719m true) (l71c 0) (l71m true) (l720c 4) (l720m false) (l721c 4) (l721m false) (l722c 1) (l722m true) (l723c 0) (l723m false) (l724c 2) (l724m true) (l725c 0) (l725m false) (l726c 2) (l726m true) (l727c 2) (l727m true) (l728c 0) (l728m false) (l729c 0) (l729m false) (l72c 0) (l72m true) (l730c 1) (l730m true) (l731c 2) (l731m true) (l732c 2) (l732m false) (l733c 2) (l733m false) (l734c 2) (l734m true) (l735c 1) (l735m true) (l736c 2) (l736m true) (l737c 2) (l737m true) (l738c 1) (l738m true) (l739c 3) (l739m true) (l73c 0) (l73m true) (l740c 2) (l740m true) (l741c 3) (l741m true) (l742c 0) (l742m false) (l743c 2) (l743m true) (l744c 3) (l744m true) (l745c 0) (l745m false) (l746c 2) (l746m false) (l747c 2) (l747m false) (l748c 2) (l748m true) (l749c 2) (l749m false) (l74c 7) (l74m true) (l750c 5) (l750m true) (l751c 1) (l751m true) (l752c 3) (l752m false) (l753c 3) (l753m false) (l754c 3) (l754m true) (l755c 5) (l755m true) (l756c 1) (l756m false) (l757c 1) (l757m false) (l758c 1) (l758m false) (l759c 2) (l759m true) (l75c 0) (l75m true) (l760c 1) (l760m true) (l761c 1) (l761m false) (l762c 3) (l762m false) (l763c 1) (l763m false) (l764c 1) (l764m false) (l765c 5) (l765m true) (l766c 0) (l766m false) (l767c 4) (l767m true) (l768c 0) (l768m false) (l769c 3) (l769m true) (l76c 0) (l76m true) (l770c 2) (l770m false) (l771c 2) (l771m false) (l772c 2) (l772m false) (l773c 3) (l773m true) (l774c 2) (l774m true) (l775c 4) (l775m false) (l776c 4) (l776m false) (l777c 4) (l777m true) (l778c 5) (l778m true) (l779c 5) (l779m true) (l77c 0) (l77m true) (l780c 5) (l780m true) (l781c 4) (l781m true) (l782c 0) (l782m true) (l783c 0) (l783m false) (l784c 0) (l784m false) (l785c 4) (l785m true) (l786c 3) (l786m true) (l787c 2) (l787m false) (l788c 2) (l788m false) (l789c 2) (l789m false) (l78c 6) (l78m true) (l790c 2) (l790m false) (l791c 4) (l791m true) (l792c 2) (l792m false) (l793c 4) (l793m false) (l794c 4) (l794m false) (l795c 3) (l795m true) (l796c 4) (l796m false) (l797c 0) (l797m false) (l798c 4) (l798m true) (l799c 3) (l799m true) (l79c 0) (l79m true) (l7c 0) (l7m false) (l800c 0) (l800m false) (l801c 5) (l801m true) (l802c 1) (l802m false) (l803c 3) (l803m false) (l804c 3) (l804m false) (l805c 3) (l805m true) (l806c 5) (l806m true) (l807c 1) (l807m false) (l808c 1) (l808m false) (l809c 3) (l809m false) (l80c 0) (l80m true) (l810c 3) (l810m false) (l811c 5) (l811m true) (l812c 3) (l812m false) (l813c 3) (l813m false) (l814c 1) (l814m false) (l815c 3) (l815m false) (l816c 3) (l816m true) (l817c 2) (l817m true) (l818c 2) (l818m false) (l819c 2) (l819m false) (l81c 0) (l81m true) (l820c 3) (l820m true) (l821c 4) (l821m true) (l822c 4) (l822m false) (l823c 4) (l823m false) (l824c 0) (l824m true) (l825c 0) (l825m false) (l826c 0) (l826m true) (l827c 0) (l827m false) (l828c 1) (l828m true) (l829c 0) (l829m true) (l82c 6) (l82m true) (l830c 0) (l830m false) (l831c 0) (l831m false) (l832c 2) (l832m true) (l833c 2) (l833m true) (l834c 2) (l834m false) (l835c 2) (l835m false) (l836c 2) (l836m true) (l837c 1) (l837m true) (l838c 2) (l838m true) (l839c 2) (l839m true) (l83c 0) (l83m true) (l840c 4) (l840m true) (l841c 3) (l841m true) (l842c 2) (l842m true) (l843c 4) (l843m true) (l844c 0) (l844m false) (l845c 0) (l845m true) (l846c 0) (l846m true) (l847c 0) (l847m false) (l848c 2) (l848m false) (l849c 2) (l849m false) (l84c 0) (l84m true) (l850c 2) (l850m true) (l851c 2) (l851m false) (l852c 3) (l852m true) (l853c 1) (l853m true) (l854c 3) (l854m false) (l855c 3) (l855m false) (l856c 3) (l856m true) (l857c 4) (l857m true) (l858c 1) (l858m false) (l859c 1) (l859m false) (l85c 0) (l85m true) (l860c 1) (l860m false) (l861c 1) (l861m true) (l862c 5) (l862m true) (l863c 1) (l863m false) (l864c 3) (l864m false) (l865c 1) (l865m false) (l866c 1) (l866m false) (l867c 2) (l867m true) (l868c 0) (l868m false) (l869c 3) (l869m true) (l86c 7) (l86m true) (l870c 0) (l870m false) (l871c 1) (l871m true) (l872c 2) (l872m false) (l873c 2) (l873m false) (l874c 2) (l874m false) (l875c 2) (l875m true) (l876c 0) (l876m true) (l877c 2) (l877m true) (l878c 2) (l878m true) (l879c 3) (l879m true) (l87c 5) (l87m false) (l880c 0) (l880m true) (l881c 1) (l881m true) (l882c 3) (l882m true) (l883c 0) (l883m true) (l884c 3) (l884m true) (l885c 0) (l885m false) (l886c 0) (l886m false) (l887c 5) (l887m true) (l888c 0) (l888m true) (l889c 2) (l889m true) (l88c 4) (l88m false) (l890c 4) (l890m true) (l891c 2) (l891m false) (l892c 2) (l892m false) (l893c 2) (l893m true) (l894c 2) (l894m false) (l895c 0) (l895m true) (l896c 4) (l896m false) (l897c 1) (l897m true) (l898c 4) (l898m false) (l899c 0) (l899m false) (l89c 4) (l89m true) (l8c 2) (l8m false) (l900c 2) (l900m true) (l901c 2) (l901m true) (l902c 0) (l902m false) (l903c 4) (l903m true) (l904c 5) (l904m true) (l905c 3) (l905m true) (l906c 3) (l906m true) (l907c 2) (l907m true) (l908c 2) (l908m true) (l909c 2) (l909m true) (l90c 5) (l90m false) (l910c 1) (l910m true) (l911c 3) (l911m false) (l912c 2) (l912m true) (l913c 5) (l913m true) (l914c 3) (l914m false) (l915c 1) (l915m false) (l916c 1) (l916m true) (l917c 3) (l917m false) (l918c 2) (l918m false) (l919c 3) (l919m true) (l91c 0) (l91m true) (l920c 2) (l920m false) (l921c 2) (l921m false) (l922c 4) (l922m false) (l923c 1) (l923m true) (l924c 4) (l924m false) (l925c 4) (l925m false) (l926c 3) (l926m true) (l927c 2) (l927m true) (l928c 0) (l928m false) (l929c 0) (l929m false) (l92c 6) (l92m true) (l930c 0) (l930m false) (l931c 3) (l931m true) (l932c 4) (l932m true) (l933c 0) (l933m false) (l934c 2) (l934m false) (l935c 2) (l935m false) (l936c 4) (l936m true) (l937c 2) (l937m false) (l938c 2) (l938m true) (l939c 4) (l939m true) (l93c 5) (l93m true) (l940c 5) (l940m true) (l941c 2) (l941m true) (l942c 5) (l942m true) (l943c 3) (l943m true) (l944c 5) (l944m true) (l945c 4) (l945m true) (l946c 3) (l946m true) (l947c 0) (l947m false) (l948c 3) (l948m true) (l949c 0) (l949m false) (l94c 1) (l94m true) (l950c 4) (l950m true) (l951c 2) (l951m true) (l952c 5) (l952m true) (l953c 2) (l953m true) (l954c 3) (l954m false) (l955c 3) (l955m true) (l956c 3) (l956m false) (l957c 3) (l957m false) (l958c 1) (l958m false) (l959c 3) (l959m true) (l95c 1) (l95m true) (l960c 4) (l960m true) (l961c 1) (l961m false) (l962c 5) (l962m true) (l963c 1) (l963m true) (l964c 5) (l964m true) (l965c 1) (l965m true) (l966c 3) (l966m false) (l967c 1) (l967m false) (l968c 1) (l968m true) (l96c 1) (l96m true) (l97c 5) (l97m true) (l98c 0) (l98m true) (l99c 5) (l99m false) (l9c 2) (l9m true))