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