sat ((f0c 0) (f0m false) (f100c 0) (f100m true) (f101c 0) (f101m true) (f102c 0) (f102m true) (f103c 0) (f103m true) (f104c 0) (f104m false) (f105c 0) (f105m false) (f106c 3) (f106m true) (f107c 3) (f107m true) (f108c 3) (f108m true) (f109c 1) (f109m true) (f10c 0) (f10m true) (f110c 0) (f110m true) (f111c 0) (f111m true) (f112c 0) (f112m false) (f113c 0) (f113m false) (f114c 0) (f114m true) (f115c 0) (f115m true) (f116c 0) (f116m true) (f117c 0) (f117m true) (f118c 0) (f118m true) (f119c 0) (f119m true) (f11c 1) (f11m false) (f120c 0) (f120m false) (f121c 0) (f121m false) (f122c 0) (f122m true) (f123c 0) (f123m true) (f124c 0) (f124m true) (f125c 0) (f125m true) (f126c 0) (f126m true) (f127c 0) (f127m true) (f128c 0) (f128m false) (f129c 0) (f129m false) (f12c 0) (f12m true) (f130c 0) (f130m true) (f131c 0) (f131m true) (f132c 0) (f132m true) (f133c 0) (f133m true) (f134c 1) (f134m false) (f135c 0) (f135m false) (f136c 1) (f136m false) (f137c 1) (f137m false) (f138c 0) (f138m true) (f139c 0) (f139m true) (f13c 0) (f13m true) (f140c 0) (f140m true) (f141c 0) (f141m true) (f142c 0) (f142m true) (f143c 0) (f143m true) (f144c 0) (f144m false) (f145c 0) (f145m false) (f146c 0) (f146m true) (f147c 0) (f147m true) (f148c 0) (f148m true) (f149c 0) (f149m true) (f14c 0) (f14m true) (f150c 1) (f150m false) (f151c 0) (f151m false) (f152c 1) (f152m false) (f153c 1) (f153m false) (f154c 0) (f154m true) (f155c 0) (f155m true) (f156c 0) (f156m true) (f157c 0) (f157m true) (f158c 0) (f158m true) (f159c 0) (f159m true) (f15c 0) (f15m true) (f160c 0) (f160m false) (f161c 0) (f161m false) (f162c 0) (f162m true) (f163c 0) (f163m true) (f164c 0) (f164m true) (f165c 0) (f165m true) (f166c 0) (f166m true) (f167c 0) (f167m true) (f168c 0) (f168m false) (f169c 0) (f169m false) (f16c 0) (f16m false) (f170c 0) (f170m true) (f171c 0) (f171m true) (f172c 0) (f172m true) (f173c 0) (f173m true) (f174c 1) (f174m false) (f175c 0) (f175m false) (f176c 1) (f176m false) (f177c 1) (f177m false) (f178c 1) (f178m true) (f179c 3) (f179m true) (f17c 0) (f17m false) (f180c 1) (f180m true) (f181c 3) (f181m true) (f182c 0) (f182m true) (f183c 0) (f183m true) (f184c 0) (f184m false) (f185c 0) (f185m false) (f186c 0) (f186m true) (f187c 0) (f187m true) (f188c 0) (f188m true) (f189c 0) (f189m true) (f18c 0) (f18m true) (f190c 0) (f190m true) (f191c 0) (f191m true) (f192c 0) (f192m false) (f193c 0) (f193m false) (f194c 0) (f194m true) (f195c 0) (f195m true) (f196c 0) (f196m true) (f197c 0) (f197m true) (f198c 1) (f198m false) (f199c 0) (f199m false) (f19c 0) (f19m true) (f1c 0) (f1m false) (f200c 1) (f200m false) (f201c 1) (f201m false) (f202c 0) (f202m true) (f203c 0) (f203m true) (f204c 0) (f204m true) (f205c 0) (f205m true) (f206c 0) (f206m true) (f207c 0) (f207m true) (f208c 0) (f208m false) (f209c 0) (f209m false) (f20c 0) (f20m true) (f210c 0) (f210m true) (f211c 0) (f211m true) (f212c 0) (f212m true) (f213c 0) (f213m true) (f214c 0) (f214m true) (f215c 0) (f215m true) (f216c 0) (f216m false) (f217c 0) (f217m false) (f21c 0) (f21m true) (f22c 1) (f22m false) (f23c 0) (f23m false) (f24c 1) (f24m false) (f25c 1) (f25m false) (f26c 0) (f26m true) (f27c 0) (f27m true) (f28c 0) (f28m true) (f29c 0) (f29m true) (f2c 0) (f2m false) (f30c 0) (f30m true) (f31c 0) (f31m true) (f32c 0) (f32m false) (f33c 0) (f33m false) (f34c 0) (f34m true) (f35c 0) (f35m true) (f36c 0) (f36m true) (f37c 0) (f37m true) (f38c 0) (f38m true) (f39c 0) (f39m true) (f3c 0) (f3m true) (f40c 0) (f40m false) (f41c 0) (f41m false) (f42c 0) (f42m true) (f43c 0) (f43m true) (f44c 0) (f44m true) (f45c 0) (f45m true) (f46c 1) (f46m false) (f47c 0) (f47m false) (f48c 1) (f48m false) (f49c 1) (f49m false) (f4c 0) (f4m false) (f50c 3) (f50m true) (f51c 3) (f51m true) (f52c 3) (f52m true) (f53c 3) (f53m true) (f54c 1) (f54m false) (f55c 1) (f55m false) (f56c 1) (f56m false) (f57c 1) (f57m false) (f58c 0) (f58m true) (f59c 0) (f59m true) (f5c 0) (f5m true) (f60c 0) (f60m true) (f61c 0) (f61m true) (f62c 0) (f62m true) (f63c 0) (f63m true) (f64c 0) (f64m false) (f65c 0) (f65m false) (f66c 0) (f66m true) (f67c 0) (f67m true) (f68c 0) (f68m true) (f69c 0) (f69m true) (f6c 0) (f6m false) (f70c 1) (f70m false) (f71c 0) (f71m false) (f72c 1) (f72m false) (f73c 1) (f73m false) (f74c 0) (f74m true) (f75c 0) (f75m true) (f76c 0) (f76m true) (f77c 0) (f77m true) (f78c 0) (f78m true) (f79c 0) (f79m true) (f7c 1) (f7m false) (f80c 0) (f80m false) (f81c 0) (f81m false) (f82c 0) (f82m true) (f83c 0) (f83m true) (f84c 0) (f84m true) (f85c 0) (f85m true) (f86c 0) (f86m false) (f87c 0) (f87m false) (f88c 0) (f88m false) (f89c 0) (f89m false) (f8c 1) (f8m true) (f90c 0) (f90m true) (f91c 0) (f91m true) (f92c 0) (f92m true) (f93c 0) (f93m true) (f94c 0) (f94m true) (f95c 0) (f95m true) (f96c 0) (f96m false) (f97c 0) (f97m false) (f98c 0) (f98m true) (f99c 0) (f99m true) (f9c 0) (f9m false) (l0c 0) (l0m true) (l100c 0) (l100m true) (l101c 0) (l101m true) (l102c 0) (l102m true) (l103c 0) (l103m true) (l104c 0) (l104m true) (l105c 0) (l105m true) (l106c 0) (l106m true) (l107c 0) (l107m true) (l108c 0) (l108m true) (l109c 0) (l109m true) (l10c 0) (l10m true) (l110c 1) (l110m true) (l111c 0) (l111m true) (l112c 0) (l112m true) (l113c 0) (l113m true) (l114c 0) (l114m true) (l115c 0) (l115m true) (l116c 0) (l116m true) (l117c 0) (l117m true) (l118c 0) (l118m false) (l119c 0) (l119m false) (l11c 0) (l11m true) (l120c 0) (l120m true) (l121c 0) (l121m true) (l122c 0) (l122m true) (l123c 0) (l123m true) (l124c 0) (l124m true) (l125c 0) (l125m true) (l126c 0) (l126m true) (l127c 0) (l127m true) (l128c 0) (l128m true) (l129c 0) (l129m true) (l12c 0) (l12m false) (l130c 0) (l130m true) (l131c 0) (l131m true) (l132c 0) (l132m false) (l133c 1) (l133m false) (l134c 1) (l134m false) (l135c 0) (l135m true) (l136c 0) (l136m false) (l137c 0) (l137m false) (l138c 1) (l138m false) (l139c 1) (l139m false) (l13c 1) (l13m false) (l140c 0) (l140m true) (l141c 0) (l141m true) (l142c 0) (l142m true) (l143c 0) (l143m true) (l144c 0) (l144m true) (l145c 0) (l145m true) (l146c 0) (l146m true) (l147c 0) (l147m true) (l148c 0) (l148m true) (l149c 0) (l149m true) (l14c 1) (l14m false) (l150c 0) (l150m true) (l151c 0) (l151m true) (l152c 0) (l152m true) (l153c 0) (l153m true) (l154c 0) (l154m true) (l155c 0) (l155m true) (l156c 0) (l156m true) (l157c 0) (l157m true) (l158c 0) (l158m false) (l159c 0) (l159m false) (l15c 0) (l15m true) (l160c 0) (l160m true) (l161c 0) (l161m true) (l162c 0) (l162m true) (l163c 0) (l163m true) (l164c 0) (l164m true) (l165c 0) (l165m true) (l166c 0) (l166m true) (l167c 0) (l167m true) (l168c 0) (l168m true) (l169c 0) (l169m true) (l16c 0) (l16m false) (l170c 0) (l170m true) (l171c 0) (l171m true) (l172c 0) (l172m false) (l173c 0) (l173m false) (l174c 0) (l174m false) (l175c 0) (l175m false) (l176c 0) (l176m true) (l177c 0) (l177m false) (l178c 0) (l178m false) (l179c 0) (l179m false) (l17c 0) (l17m false) (l180c 0) (l180m true) (l181c 0) (l181m true) (l182c 0) (l182m true) (l183c 0) (l183m true) (l184c 0) (l184m true) (l185c 0) (l185m true) (l186c 0) (l186m true) (l187c 0) (l187m true) (l188c 0) (l188m true) (l189c 0) (l189m true) (l18c 1) (l18m false) (l190c 0) (l190m true) (l191c 0) (l191m true) (l192c 0) (l192m true) (l193c 0) (l193m true) (l194c 0) (l194m true) (l195c 0) (l195m true) (l196c 0) (l196m true) (l197c 0) (l197m true) (l198c 0) (l198m false) (l199c 0) (l199m false) (l19c 1) (l19m false) (l1c 0) (l1m true) (l200c 0) (l200m true) (l201c 0) (l201m true) (l202c 0) (l202m true) (l203c 0) (l203m true) (l204c 0) (l204m true) (l205c 0) (l205m true) (l206c 0) (l206m true) (l207c 0) (l207m true) (l208c 0) (l208m true) (l209c 0) (l209m true) (l20c 0) (l20m true) (l210c 0) (l210m true) (l211c 0) (l211m true) (l212c 0) (l212m true) (l213c 0) (l213m true) (l214c 0) (l214m true) (l215c 0) (l215m true) (l216c 0) (l216m true) (l217c 0) (l217m true) (l218c 0) (l218m false) (l219c 0) (l219m false) (l21c 0) (l21m true) (l220c 0) (l220m true) (l221c 0) (l221m true) (l222c 3) (l222m true) (l223c 0) (l223m true) (l224c 0) (l224m true) (l225c 3) (l225m true) (l226c 0) (l226m true) (l227c 0) (l227m true) (l228c 3) (l228m true) (l229c 0) (l229m true) (l22c 0) (l22m true) (l230c 0) (l230m true) (l231c 1) (l231m true) (l232c 0) (l232m true) (l233c 0) (l233m true) (l234c 0) (l234m true) (l235c 0) (l235m true) (l236c 0) (l236m true) (l237c 0) (l237m true) (l238c 0) (l238m false) (l239c 0) (l239m false) (l23c 0) (l23m true) (l240c 0) (l240m true) (l241c 0) (l241m true) (l242c 0) (l242m true) (l243c 0) (l243m true) (l244c 0) (l244m true) (l245c 0) (l245m true) (l246c 0) (l246m true) (l247c 0) (l247m true) (l248c 0) (l248m true) (l249c 0) (l249m true) (l24c 0) (l24m true) (l250c 0) (l250m true) (l251c 0) (l251m true) (l252c 0) (l252m true) (l253c 0) (l253m true) (l254c 0) (l254m true) (l255c 0) (l255m true) (l256c 0) (l256m true) (l257c 0) (l257m true) (l258c 0) (l258m false) (l259c 0) (l259m false) (l25c 0) (l25m true) (l260c 0) (l260m true) (l261c 0) (l261m true) (l262c 0) (l262m true) (l263c 0) (l263m true) (l264c 0) (l264m true) (l265c 0) (l265m true) (l266c 0) (l266m true) (l267c 0) (l267m true) (l268c 0) (l268m true) (l269c 0) (l269m true) (l26c 0) (l26m true) (l270c 0) (l270m true) (l271c 0) (l271m true) (l272c 0) (l272m true) (l273c 0) (l273m true) (l274c 0) (l274m true) (l275c 0) (l275m true) (l276c 0) (l276m true) (l277c 0) (l277m true) (l278c 0) (l278m false) (l279c 0) (l279m false) (l27c 0) (l27m true) (l280c 0) (l280m true) (l281c 0) (l281m true) (l282c 0) (l282m true) (l283c 0) (l283m true) (l284c 0) (l284m true) (l285c 0) (l285m true) (l286c 0) (l286m true) (l287c 0) (l287m true) (l288c 0) (l288m true) (l289c 0) (l289m true) (l28c 0) (l28m true) (l290c 0) (l290m true) (l291c 0) (l291m true) (l292c 0) (l292m false) (l293c 1) (l293m false) (l294c 1) (l294m false) (l295c 0) (l295m true) (l296c 0) (l296m false) (l297c 0) (l297m false) (l298c 1) (l298m false) (l299c 1) (l299m false) (l29c 0) (l29m true) (l2c 0) (l2m true) (l300c 0) (l300m true) (l301c 0) (l301m true) (l302c 0) (l302m true) (l303c 0) (l303m true) (l304c 0) (l304m true) (l305c 0) (l305m true) (l306c 0) (l306m true) (l307c 0) (l307m true) (l308c 0) (l308m true) (l309c 0) (l309m true) (l30c 0) (l30m true) (l310c 0) (l310m true) (l311c 0) (l311m true) (l312c 0) (l312m true) (l313c 0) (l313m true) (l314c 0) (l314m true) (l315c 0) (l315m true) (l316c 0) (l316m true) (l317c 0) (l317m true) (l318c 0) (l318m false) (l319c 0) (l319m false) (l31c 0) (l31m true) (l320c 0) (l320m true) (l321c 0) (l321m true) (l322c 0) (l322m true) (l323c 0) (l323m true) (l324c 0) (l324m true) (l325c 0) (l325m true) (l326c 0) (l326m true) (l327c 0) (l327m true) (l328c 0) (l328m true) (l329c 0) (l329m true) (l32c 0) (l32m true) (l330c 0) (l330m true) (l331c 0) (l331m true) (l332c 0) (l332m false) (l333c 1) (l333m false) (l334c 1) (l334m false) (l335c 0) (l335m true) (l336c 0) (l336m false) (l337c 0) (l337m false) (l338c 1) (l338m false) (l339c 1) (l339m false) (l33c 0) (l33m true) (l340c 0) (l340m true) (l341c 0) (l341m true) (l342c 0) (l342m true) (l343c 0) (l343m true) (l344c 0) (l344m true) (l345c 0) (l345m true) (l346c 0) (l346m true) (l347c 0) (l347m true) (l348c 0) (l348m true) (l349c 0) (l349m true) (l34c 0) (l34m true) (l350c 0) (l350m true) (l351c 0) (l351m true) (l352c 0) (l352m true) (l353c 0) (l353m true) (l354c 0) (l354m true) (l355c 0) (l355m true) (l356c 0) (l356m true) (l357c 0) (l357m true) (l358c 0) (l358m false) (l359c 0) (l359m false) (l35c 0) (l35m true) (l360c 0) (l360m true) (l361c 0) (l361m true) (l362c 0) (l362m true) (l363c 0) (l363m true) (l364c 0) (l364m true) (l365c 0) (l365m true) (l366c 0) (l366m true) (l367c 0) (l367m true) (l368c 0) (l368m true) (l369c 0) (l369m true) (l36c 0) (l36m true) (l370c 0) (l370m true) (l371c 0) (l371m true) (l372c 0) (l372m true) (l373c 0) (l373m true) (l374c 0) (l374m true) (l375c 0) (l375m true) (l376c 0) (l376m true) (l377c 0) (l377m true) (l378c 0) (l378m false) (l379c 0) (l379m false) (l37c 0) (l37m true) (l380c 0) (l380m true) (l381c 0) (l381m true) (l382c 0) (l382m true) (l383c 0) (l383m true) (l384c 0) (l384m true) (l385c 0) (l385m true) (l386c 0) (l386m true) (l387c 0) (l387m true) (l388c 0) (l388m true) (l389c 0) (l389m true) (l38c 0) (l38m false) (l390c 0) (l390m true) (l391c 0) (l391m true) (l392c 0) (l392m false) (l393c 1) (l393m false) (l394c 1) (l394m false) (l395c 0) (l395m true) (l396c 0) (l396m false) (l397c 0) (l397m false) (l398c 1) (l398m false) (l399c 1) (l399m false) (l39c 0) (l39m false) (l3c 0) (l3m true) (l400c 0) (l400m true) (l401c 0) (l401m true) (l402c 1) (l402m true) (l403c 0) (l403m true) (l404c 0) (l404m true) (l405c 3) (l405m true) (l406c 0) (l406m true) (l407c 0) (l407m true) (l408c 1) (l408m true) (l409c 0) (l409m true) (l40c 0) (l40m true) (l410c 0) (l410m true) (l411c 3) (l411m true) (l412c 0) (l412m true) (l413c 0) (l413m true) (l414c 0) (l414m true) (l415c 0) (l415m true) (l416c 0) (l416m true) (l417c 0) (l417m true) (l418c 0) (l418m false) (l419c 0) (l419m false) (l41c 0) (l41m true) (l420c 0) (l420m true) (l421c 0) (l421m true) (l422c 0) (l422m true) (l423c 0) (l423m true) (l424c 0) (l424m true) (l425c 0) (l425m true) (l426c 0) (l426m true) (l427c 0) (l427m true) (l428c 0) (l428m true) (l429c 0) (l429m true) (l42c 0) (l42m true) (l430c 0) (l430m true) (l431c 0) (l431m true) (l432c 0) (l432m true) (l433c 0) (l433m true) (l434c 0) (l434m true) (l435c 0) (l435m true) (l436c 0) (l436m true) (l437c 0) (l437m true) (l438c 0) (l438m false) (l439c 0) (l439m false) (l43c 0) (l43m true) (l440c 0) (l440m true) (l441c 0) (l441m true) (l442c 0) (l442m true) (l443c 0) (l443m true) (l444c 0) (l444m true) (l445c 0) (l445m true) (l446c 0) (l446m true) (l447c 0) (l447m true) (l448c 0) (l448m true) (l449c 0) (l449m true) (l44c 0) (l44m true) (l450c 0) (l450m true) (l451c 0) (l451m true) (l452c 0) (l452m false) (l453c 1) (l453m false) (l454c 1) (l454m false) (l455c 0) (l455m true) (l456c 0) (l456m false) (l457c 0) (l457m false) (l458c 1) (l458m false) (l459c 1) (l459m false) (l45c 0) (l45m true) (l460c 0) (l460m true) (l461c 0) (l461m true) (l462c 0) (l462m true) (l463c 0) (l463m true) (l464c 0) (l464m true) (l465c 0) (l465m true) (l466c 0) (l466m true) (l467c 0) (l467m true) (l468c 0) (l468m true) (l469c 0) (l469m true) (l46c 0) (l46m true) (l470c 0) (l470m true) (l471c 0) (l471m true) (l472c 0) (l472m true) (l473c 0) (l473m true) (l474c 0) (l474m true) (l475c 0) (l475m true) (l476c 0) (l476m true) (l477c 0) (l477m true) (l478c 0) (l478m false) (l479c 0) (l479m false) (l47c 0) (l47m true) (l480c 0) (l480m true) (l481c 0) (l481m true) (l482c 0) (l482m true) (l483c 0) (l483m true) (l484c 0) (l484m true) (l485c 0) (l485m true) (l486c 0) (l486m true) (l487c 0) (l487m true) (l488c 0) (l488m true) (l489c 0) (l489m true) (l48c 0) (l48m true) (l490c 0) (l490m true) (l491c 0) (l491m true) (l492c 0) (l492m true) (l493c 0) (l493m true) (l494c 0) (l494m true) (l495c 0) (l495m true) (l496c 0) (l496m true) (l497c 0) (l497m true) (l498c 0) (l498m false) (l499c 0) (l499m false) (l49c 0) (l49m true) (l4c 0) (l4m true) (l50c 0) (l50m true) (l51c 0) (l51m true) (l52c 0) (l52m true) (l53c 0) (l53m true) (l54c 0) (l54m true) (l55c 0) (l55m true) (l56c 0) (l56m true) (l57c 0) (l57m true) (l58c 0) (l58m false) (l59c 0) (l59m false) (l5c 0) (l5m true) (l60c 0) (l60m true) (l61c 0) (l61m true) (l62c 0) (l62m true) (l63c 0) (l63m true) (l64c 0) (l64m true) (l65c 0) (l65m true) (l66c 0) (l66m true) (l67c 0) (l67m true) (l68c 0) (l68m true) (l69c 0) (l69m true) (l6c 0) (l6m true) (l70c 0) (l70m true) (l71c 0) (l71m true) (l72c 0) (l72m false) (l73c 1) (l73m false) (l74c 1) (l74m false) (l75c 0) (l75m true) (l76c 0) (l76m false) (l77c 0) (l77m false) (l78c 1) (l78m false) (l79c 1) (l79m false) (l7c 0) (l7m true) (l80c 0) (l80m true) (l81c 0) (l81m true) (l82c 3) (l82m true) (l83c 0) (l83m true) (l84c 0) (l84m true) (l85c 3) (l85m true) (l86c 0) (l86m true) (l87c 0) (l87m true) (l88c 3) (l88m true) (l89c 0) (l89m true) (l8c 0) (l8m true) (l90c 0) (l90m true) (l91c 3) (l91m true) (l92c 1) (l92m false) (l93c 1) (l93m false) (l94c 1) (l94m false) (l95c 1) (l95m false) (l96c 0) (l96m true) (l97c 1) (l97m false) (l98c 1) (l98m false) (l99c 1) (l99m false) (l9c 0) (l9m true))