sat ((f0m false) (f0c 0) (f1m true) (f1c 59) (f2m true) (f2c 55) (f3m true) (f3c 92) (f4m true) (f4c 38) (f5m true) (f5c 93) (f6m false) (f6c (- 50)) (f7m false) (f7c 37) (f8m false) (f8c (- 136)) (f9m false) (f9c (- 31)) (f10m false) (f10c 36) (f11m false) (f11c 0) (f12m true) (f12c 65) (f13m true) (f13c 36) (f14m false) (f14c (- 37)) (f15m true) (f15c 53) (f16m false) (f16c 36) (f17m false) (f17c (- 51)) (f18m false) (f18c (- 61)) (f19m false) (f19c (- 25)) (f20m true) (f20c (- 52)) (f21m true) (f21c 0) (f22m false) (f22c 37) (f23m true) (f23c 92) (f24m false) (f24c 0) (f25m true) (f25c 92) (f26m false) (f26c (- 68)) (f27m true) (f27c 20) (f28m false) (f28c (- 14)) (f29m false) (f29c (- 82)) (f30m false) (f30c 36) (f31m false) (f31c 0) (f32m false) (f32c (- 31)) (f33m true) (f33c (- 45)) (f34m false) (f34c (- 99)) (f35m true) (f35c (- 82)) (f36m false) (f36c 37) (f37m false) (f37c (- 31)) (f38m false) (f38c 37) (f39m false) (f39c 0) (f40m false) (f40c (- 31)) (f41m true) (f41c (- 21)) (f42m true) (f42c (- 7)) (f43m true) (f43c 10) (f44m false) (f44c 37) (f45m true) (f45c 92) (f46m false) (f46c 37) (f47m true) (f47c 93) (f48m true) (f48c (- 100)) (f49m true) (f49c 44) (f50m false) (f50c (- 87)) (f51m false) (f51c 0) (f52m true) (f52c 101) (f53m false) (f53c (- 1)) (f54m false) (f54c 36) (f55m false) (f55c (- 1)) (f56m true) (f56c (- 35)) (f57m true) (f57c 109) (f58m true) (f58c (- 36)) (f59m true) (f59c 7) (f60m true) (f60c 36) (f61m false) (f61c (- 1)) (f62m false) (f62c 36) (f63m false) (f63c (- 1)) (f64m true) (f64c (- 96)) (f65m true) (f65c (- 20)) (f66m true) (f66c (- 8)) (f67m true) (f67c 9) (f68m false) (f68c (- 25)) (f69m true) (f69c (- 15)) (f70m false) (f70c 37) (f71m true) (f71c 92) (f72m false) (f72c 0) (f73m true) (f73c 92) (f74m false) (f74c (- 68)) (f75m true) (f75c 24) (f76m false) (f76c (- 14)) (f77m false) (f77c (- 82)) (f78m false) (f78c 36) (f79m false) (f79c 0) (f80m false) (f80c (- 31)) (f81m true) (f81c 54) (f82m false) (f82c (- 99)) (f83m true) (f83c (- 5)) (f84m false) (f84c 37) (f85m false) (f85c (- 31)) (f86m false) (f86c 37) (f87m false) (f87c 0) (f88m false) (f88c (- 31)) (f89m true) (f89c 56) (f90m true) (f90c (- 7)) (f91m true) (f91c 115) (f92m false) (f92c 37) (f93m true) (f93c 92) (f94m false) (f94c 37) (f95m true) (f95c 93) (f96m true) (f96c 13) (f97m true) (f97c 59) (f98m false) (f98c (- 87)) (f99m false) (f99c 0) (f100m true) (f100c 101) (f101m false) (f101c (- 1)) (f102m false) (f102c 36) (f103m false) (f103c (- 1)) (f104m true) (f104c (- 30)) (f105m true) (f105c 57) (f106m true) (f106c (- 8)) (f107m true) (f107c 114) (f108m false) (f108c 36) (f109m true) (f109c 91) (f110m false) (f110c 36) (f111m true) (f111c 93) (f112m true) (f112c (- 53)) (f113m true) (f113c 102) (f114m false) (f114c (- 87)) (f115m false) (f115c 0) (f116m true) (f116c 36) (f117m false) (f117c (- 1)) (f118m false) (f118c 36) (f119m false) (f119c (- 1)) (f120m false) (f120c (- 112)) (f121m false) (f121c (- 25)) (f122m true) (f122c (- 105)) (f123m true) (f123c 50) (f124m false) (f124c (- 25)) (f125m true) (f125c (- 15)) (f126m false) (f126c 37) (f127m true) (f127c 94) (f128m false) (f128c (- 99)) (f129m false) (f129c 6) (f130m false) (f130c (- 167)) (f131m false) (f131c (- 62)) (f132m false) (f132c 37) (f133m false) (f133c (- 31)) (f134m false) (f134c 37) (f135m false) (f135c 0) (f136m false) (f136c (- 130)) (f137m false) (f137c (- 25)) (f138m false) (f138c (- 198)) (f139m false) (f139c (- 93)) (f140m false) (f140c 37) (f141m false) (f141c (- 31)) (f142m false) (f142c 37) (f143m false) (f143c 0) (f144m false) (f144c (- 130)) (f145m false) (f145c (- 25)) (f146m true) (f146c (- 106)) (f147m true) (f147c 30) (f148m false) (f148c 37) (f149m true) (f149c 92) (f150m false) (f150c 37) (f151m true) (f151c 93) (f152m false) (f152c 0) (f153m true) (f153c 92) (f154m false) (f154c (- 68)) (f155m true) (f155c 24) (f156m false) (f156c (- 14)) (f157m false) (f157c (- 82)) (f158m false) (f158c 36) (f159m false) (f159c 0) (f160m false) (f160c (- 31)) (f161m true) (f161c (- 104)) (f162m false) (f162c (- 99)) (f163m true) (f163c (- 5)) (f164m false) (f164c 37) (f165m false) (f165c (- 31)) (f166m false) (f166c 37) (f167m false) (f167c 0) (f168m true) (f168c 36) (f169m true) (f169c (- 37)) (f170m false) (f170c (- 68)) (f171m true) (f171c (- 103)) (f172m true) (f172c 102) (f173m false) (f173c 0) (f174m false) (f174c 36) (f175m false) (f175c 0) (f176m true) (f176c (- 100)) (f177m true) (f177c 4) (f178m false) (f178c (- 87)) (f179m false) (f179c 0) (f180m true) (f180c 36) (f181m false) (f181c (- 1)) (f182m false) (f182c 36) (f183m false) (f183c (- 1)) (f184m true) (f184c (- 35)) (f185m true) (f185c 36) (f186m true) (f186c (- 36)) (f187m true) (f187c (- 71)) (f188m true) (f188c 35) (f189m false) (f189c (- 1)) (f190m false) (f190c 36) (f191m false) (f191c (- 1)) (f192m true) (f192c 37) (f193m true) (f193c (- 36)) (f194m true) (f194c (- 67)) (f195m true) (f195c (- 102)) (f196m false) (f196c 36) (f197m false) (f197c (- 32)) (f198m false) (f198c 36) (f199m false) (f199c 0) (f200m true) (f200c 15) (f201m true) (f201c 104) (f202m false) (f202c (- 87)) (f203m false) (f203c 0) (f204m true) (f204c 36) (f205m false) (f205c (- 1)) (f206m false) (f206c 36) (f207m false) (f207c (- 1)) (f208m false) (f208c (- 50)) (f209m false) (f209c 37) (f210m false) (f210c (- 118)) (f211m false) (f211c (- 31)) (f212m false) (f212c 36) (f213m false) (f213c (- 32)) (f214m false) (f214c 36) (f215m false) (f215c 0) (f216m false) (f216c (- 99)) (f217m false) (f217c 6) (f218m false) (f218c (- 167)) (f219m false) (f219c (- 62)) (f220m false) (f220c 37) (f221m false) (f221c (- 31)) (f222m false) (f222c 37) (f223m false) (f223c 0) (f224m false) (f224c (- 130)) (f225m false) (f225c (- 25)) (f226m false) (f226c (- 198)) (f227m false) (f227c (- 93)) (f228m false) (f228c 37) (f229m false) (f229c (- 31)) (f230m false) (f230c 37) (f231m false) (f231c 0) (f232m true) (f232c (- 65)) (f233m true) (f233c 38) (f234m false) (f234c (- 167)) (f235m false) (f235c (- 62)) (f236m true) (f236c 36) (f237m false) (f237c 0) (f238m false) (f238c 36) (f239m false) (f239c 0))