-
-
Save key-moon/aa621dea45d684255710e782c8bc51b2 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| var binary = @"[b12 = True, | |
| b37 = True, | |
| b35 = True, | |
| b46 = False, | |
| b62 = False, | |
| b58 = True, | |
| b127 = True, | |
| b67 = False, | |
| b97 = True, | |
| b16 = True, | |
| b101 = False, | |
| b63 = True, | |
| b24 = False, | |
| b43 = False, | |
| b69 = False, | |
| b103 = False, | |
| b78 = True, | |
| b111 = False, | |
| b79 = False, | |
| b110 = True, | |
| b94 = False, | |
| b52 = False, | |
| b11 = False, | |
| b73 = True, | |
| b22 = False, | |
| b102 = True, | |
| b75 = False, | |
| b85 = True, | |
| b13 = True, | |
| b15 = False, | |
| b5 = False, | |
| b100 = False, | |
| b32 = True, | |
| b117 = False, | |
| b95 = False, | |
| b119 = False, | |
| b19 = True, | |
| b71 = False, | |
| b90 = True, | |
| b40 = False, | |
| b7 = True, | |
| b87 = True, | |
| b66 = True, | |
| b8 = False, | |
| b4 = False, | |
| b121 = False, | |
| b65 = True, | |
| b68 = True, | |
| b86 = True, | |
| b124 = False, | |
| b82 = True, | |
| b60 = True, | |
| b49 = True, | |
| b74 = True, | |
| b126 = False, | |
| b31 = False, | |
| b105 = False, | |
| b116 = True, | |
| b112 = True, | |
| b44 = False, | |
| b98 = False, | |
| b48 = True, | |
| b47 = True, | |
| b9 = True, | |
| b33 = True, | |
| b88 = False, | |
| b23 = False, | |
| b96 = False, | |
| b41 = True, | |
| b28 = False, | |
| b84 = False, | |
| b39 = True, | |
| b2 = True, | |
| b81 = True, | |
| b51 = True, | |
| b123 = False, | |
| b29 = False, | |
| b83 = True, | |
| b59 = False, | |
| b26 = True, | |
| b122 = True, | |
| b64 = True, | |
| b70 = True, | |
| b92 = True, | |
| b106 = True, | |
| b18 = False, | |
| b113 = True, | |
| b42 = False, | |
| b115 = True, | |
| b118 = False, | |
| b91 = False, | |
| b108 = True, | |
| b10 = False, | |
| b1 = False, | |
| b99 = True, | |
| b21 = False, | |
| b34 = True, | |
| b53 = True, | |
| b20 = True, | |
| b3 = True, | |
| b125 = True, | |
| b89 = True, | |
| b30 = True, | |
| b114 = False, | |
| b27 = True, | |
| b38 = False, | |
| b6 = True, | |
| b104 = False, | |
| b56 = False, | |
| b61 = False, | |
| b80 = False, | |
| b107 = False, | |
| b93 = False, | |
| b25 = True, | |
| b109 = True, | |
| b17 = True, | |
| b72 = False, | |
| b36 = False, | |
| b50 = True, | |
| b57 = True, | |
| b55 = True, | |
| b120 = True, | |
| b54 = True, | |
| b0 = True, | |
| b77 = False, | |
| b45 = True, | |
| b76 = False, | |
| b14 = False]".Trim('[', ']').Split(',').Select(x => x.Split('=').Select(y => y.Trim())).Select(x => new Tuple<int, string>(int.Parse(x.First().Substring(1)), x.Last())).OrderBy(x => x.Item1).Select(x => x.Item2.Contains("True") ? "1" : "0").Reverse().Aggregate((x, y) => x + y); | |
| //binary = "10100101000110110111010001001010000101101110111001000110010101111001011011101111101000101010111101001110000110110011001011001101" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| print(int('10100101000110110111010001001010000101101110111001000110010101111001011011101111101000101010111101001110000110110011001011001101',2)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import sys | |
| from z3 import * | |
| b0 = Bool('b0') | |
| b1 = Bool('b1') | |
| b2 = Bool('b2') | |
| b3 = Bool('b3') | |
| b4 = Bool('b4') | |
| b5 = Bool('b5') | |
| b6 = Bool('b6') | |
| b7 = Bool('b7') | |
| b8 = Bool('b8') | |
| b9 = Bool('b9') | |
| b10 = Bool('b10') | |
| b11 = Bool('b11') | |
| b12 = Bool('b12') | |
| b13 = Bool('b13') | |
| b14 = Bool('b14') | |
| b15 = Bool('b15') | |
| b16 = Bool('b16') | |
| b17 = Bool('b17') | |
| b18 = Bool('b18') | |
| b19 = Bool('b19') | |
| b20 = Bool('b20') | |
| b21 = Bool('b21') | |
| b22 = Bool('b22') | |
| b23 = Bool('b23') | |
| b24 = Bool('b24') | |
| b25 = Bool('b25') | |
| b26 = Bool('b26') | |
| b27 = Bool('b27') | |
| b28 = Bool('b28') | |
| b29 = Bool('b29') | |
| b30 = Bool('b30') | |
| b31 = Bool('b31') | |
| b32 = Bool('b32') | |
| b33 = Bool('b33') | |
| b34 = Bool('b34') | |
| b35 = Bool('b35') | |
| b36 = Bool('b36') | |
| b37 = Bool('b37') | |
| b38 = Bool('b38') | |
| b39 = Bool('b39') | |
| b40 = Bool('b40') | |
| b41 = Bool('b41') | |
| b42 = Bool('b42') | |
| b43 = Bool('b43') | |
| b44 = Bool('b44') | |
| b45 = Bool('b45') | |
| b46 = Bool('b46') | |
| b47 = Bool('b47') | |
| b48 = Bool('b48') | |
| b49 = Bool('b49') | |
| b50 = Bool('b50') | |
| b51 = Bool('b51') | |
| b52 = Bool('b52') | |
| b53 = Bool('b53') | |
| b54 = Bool('b54') | |
| b55 = Bool('b55') | |
| b56 = Bool('b56') | |
| b57 = Bool('b57') | |
| b58 = Bool('b58') | |
| b59 = Bool('b59') | |
| b60 = Bool('b60') | |
| b61 = Bool('b61') | |
| b62 = Bool('b62') | |
| b63 = Bool('b63') | |
| b64 = Bool('b64') | |
| b65 = Bool('b65') | |
| b66 = Bool('b66') | |
| b67 = Bool('b67') | |
| b68 = Bool('b68') | |
| b69 = Bool('b69') | |
| b70 = Bool('b70') | |
| b71 = Bool('b71') | |
| b72 = Bool('b72') | |
| b73 = Bool('b73') | |
| b74 = Bool('b74') | |
| b75 = Bool('b75') | |
| b76 = Bool('b76') | |
| b77 = Bool('b77') | |
| b78 = Bool('b78') | |
| b79 = Bool('b79') | |
| b80 = Bool('b80') | |
| b81 = Bool('b81') | |
| b82 = Bool('b82') | |
| b83 = Bool('b83') | |
| b84 = Bool('b84') | |
| b85 = Bool('b85') | |
| b86 = Bool('b86') | |
| b87 = Bool('b87') | |
| b88 = Bool('b88') | |
| b89 = Bool('b89') | |
| b90 = Bool('b90') | |
| b91 = Bool('b91') | |
| b92 = Bool('b92') | |
| b93 = Bool('b93') | |
| b94 = Bool('b94') | |
| b95 = Bool('b95') | |
| b96 = Bool('b96') | |
| b97 = Bool('b97') | |
| b98 = Bool('b98') | |
| b99 = Bool('b99') | |
| b100 = Bool('b100') | |
| b101 = Bool('b101') | |
| b102 = Bool('b102') | |
| b103 = Bool('b103') | |
| b104 = Bool('b104') | |
| b105 = Bool('b105') | |
| b106 = Bool('b106') | |
| b107 = Bool('b107') | |
| b108 = Bool('b108') | |
| b109 = Bool('b109') | |
| b110 = Bool('b110') | |
| b111 = Bool('b111') | |
| b112 = Bool('b112') | |
| b113 = Bool('b113') | |
| b114 = Bool('b114') | |
| b115 = Bool('b115') | |
| b116 = Bool('b116') | |
| b117 = Bool('b117') | |
| b118 = Bool('b118') | |
| b119 = Bool('b119') | |
| b120 = Bool('b120') | |
| b121 = Bool('b121') | |
| b122 = Bool('b122') | |
| b123 = Bool('b123') | |
| b124 = Bool('b124') | |
| b125 = Bool('b125') | |
| b126 = Bool('b126') | |
| b127 = Bool('b127') | |
| b128 = True | |
| b129 = Xor(Xor(b0,False),Xor(b64,False)) | |
| b130 = Xor(Xor(b129,False),Xor(b128,True)) | |
| b131 = Or(Xor(b64,True),Xor(b128,False)) | |
| b132 = Or(Xor(b0,True),Xor(b128,False)) | |
| b133 = Or(Xor(b131,True),Xor(b132,True)) | |
| b134 = Or(Xor(b0,True),Xor(b64,True)) | |
| b135 = Or(Xor(b133,False),Xor(b134,True)) | |
| b136 = Xor(Xor(b1,False),Xor(b65,False)) | |
| b137 = Xor(Xor(b136,False),Xor(b135,False)) | |
| b138 = Or(Xor(b65,True),Xor(b135,True)) | |
| b139 = Or(Xor(b1,True),Xor(b135,True)) | |
| b140 = Or(Xor(b138,True),Xor(b139,True)) | |
| b141 = Or(Xor(b1,True),Xor(b65,True)) | |
| b142 = Or(Xor(b140,False),Xor(b141,True)) | |
| b143 = Xor(Xor(b2,False),Xor(b66,False)) | |
| b144 = Xor(Xor(b143,False),Xor(b142,False)) | |
| b145 = Or(Xor(b66,True),Xor(b142,True)) | |
| b146 = Or(Xor(b2,True),Xor(b142,True)) | |
| b147 = Or(Xor(b145,True),Xor(b146,True)) | |
| b148 = Or(Xor(b2,True),Xor(b66,True)) | |
| b149 = Or(Xor(b147,False),Xor(b148,True)) | |
| b150 = Xor(Xor(b3,False),Xor(b67,False)) | |
| b151 = Xor(Xor(b150,False),Xor(b149,False)) | |
| b152 = Or(Xor(b67,True),Xor(b149,True)) | |
| b153 = Or(Xor(b3,True),Xor(b149,True)) | |
| b154 = Or(Xor(b152,True),Xor(b153,True)) | |
| b155 = Or(Xor(b3,True),Xor(b67,True)) | |
| b156 = Or(Xor(b154,False),Xor(b155,True)) | |
| b157 = Xor(Xor(b4,False),Xor(b68,False)) | |
| b158 = Xor(Xor(b157,False),Xor(b156,False)) | |
| b159 = Or(Xor(b68,True),Xor(b156,True)) | |
| b160 = Or(Xor(b4,True),Xor(b156,True)) | |
| b161 = Or(Xor(b159,True),Xor(b160,True)) | |
| b162 = Or(Xor(b4,True),Xor(b68,True)) | |
| b163 = Or(Xor(b161,False),Xor(b162,True)) | |
| b164 = Xor(Xor(b5,False),Xor(b69,False)) | |
| b165 = Xor(Xor(b164,False),Xor(b163,False)) | |
| b166 = Or(Xor(b69,True),Xor(b163,True)) | |
| b167 = Or(Xor(b5,True),Xor(b163,True)) | |
| b168 = Or(Xor(b166,True),Xor(b167,True)) | |
| b169 = Or(Xor(b5,True),Xor(b69,True)) | |
| b170 = Or(Xor(b168,False),Xor(b169,True)) | |
| b171 = Xor(Xor(b6,False),Xor(b70,False)) | |
| b172 = Xor(Xor(b171,False),Xor(b170,False)) | |
| b173 = Or(Xor(b70,True),Xor(b170,True)) | |
| b174 = Or(Xor(b6,True),Xor(b170,True)) | |
| b175 = Or(Xor(b173,True),Xor(b174,True)) | |
| b176 = Or(Xor(b6,True),Xor(b70,True)) | |
| b177 = Or(Xor(b175,False),Xor(b176,True)) | |
| b178 = Xor(Xor(b7,False),Xor(b71,False)) | |
| b179 = Xor(Xor(b178,False),Xor(b177,False)) | |
| b180 = Or(Xor(b71,True),Xor(b177,True)) | |
| b181 = Or(Xor(b7,True),Xor(b177,True)) | |
| b182 = Or(Xor(b180,True),Xor(b181,True)) | |
| b183 = Or(Xor(b7,True),Xor(b71,True)) | |
| b184 = Or(Xor(b182,False),Xor(b183,True)) | |
| b185 = Xor(Xor(b8,False),Xor(b72,False)) | |
| b186 = Xor(Xor(b185,False),Xor(b184,False)) | |
| b187 = Or(Xor(b72,True),Xor(b184,True)) | |
| b188 = Or(Xor(b8,True),Xor(b184,True)) | |
| b189 = Or(Xor(b187,True),Xor(b188,True)) | |
| b190 = Or(Xor(b8,True),Xor(b72,True)) | |
| b191 = Or(Xor(b189,False),Xor(b190,True)) | |
| b192 = Xor(Xor(b9,False),Xor(b73,False)) | |
| b193 = Xor(Xor(b192,False),Xor(b191,False)) | |
| b194 = Or(Xor(b73,True),Xor(b191,True)) | |
| b195 = Or(Xor(b9,True),Xor(b191,True)) | |
| b196 = Or(Xor(b194,True),Xor(b195,True)) | |
| b197 = Or(Xor(b9,True),Xor(b73,True)) | |
| b198 = Or(Xor(b196,False),Xor(b197,True)) | |
| b199 = Xor(Xor(b10,False),Xor(b74,False)) | |
| b200 = Xor(Xor(b199,False),Xor(b198,False)) | |
| b201 = Or(Xor(b74,True),Xor(b198,True)) | |
| b202 = Or(Xor(b10,True),Xor(b198,True)) | |
| b203 = Or(Xor(b201,True),Xor(b202,True)) | |
| b204 = Or(Xor(b10,True),Xor(b74,True)) | |
| b205 = Or(Xor(b203,False),Xor(b204,True)) | |
| b206 = Xor(Xor(b11,False),Xor(b75,False)) | |
| b207 = Xor(Xor(b206,False),Xor(b205,False)) | |
| b208 = Or(Xor(b75,True),Xor(b205,True)) | |
| b209 = Or(Xor(b11,True),Xor(b205,True)) | |
| b210 = Or(Xor(b208,True),Xor(b209,True)) | |
| b211 = Or(Xor(b11,True),Xor(b75,True)) | |
| b212 = Or(Xor(b210,False),Xor(b211,True)) | |
| b213 = Xor(Xor(b12,False),Xor(b76,False)) | |
| b214 = Xor(Xor(b213,False),Xor(b212,False)) | |
| b215 = Or(Xor(b76,True),Xor(b212,True)) | |
| b216 = Or(Xor(b12,True),Xor(b212,True)) | |
| b217 = Or(Xor(b215,True),Xor(b216,True)) | |
| b218 = Or(Xor(b12,True),Xor(b76,True)) | |
| b219 = Or(Xor(b217,False),Xor(b218,True)) | |
| b220 = Xor(Xor(b13,False),Xor(b77,False)) | |
| b221 = Xor(Xor(b220,False),Xor(b219,False)) | |
| b222 = Or(Xor(b77,True),Xor(b219,True)) | |
| b223 = Or(Xor(b13,True),Xor(b219,True)) | |
| b224 = Or(Xor(b222,True),Xor(b223,True)) | |
| b225 = Or(Xor(b13,True),Xor(b77,True)) | |
| b226 = Or(Xor(b224,False),Xor(b225,True)) | |
| b227 = Xor(Xor(b14,False),Xor(b78,False)) | |
| b228 = Xor(Xor(b227,False),Xor(b226,False)) | |
| b229 = Or(Xor(b78,True),Xor(b226,True)) | |
| b230 = Or(Xor(b14,True),Xor(b226,True)) | |
| b231 = Or(Xor(b229,True),Xor(b230,True)) | |
| b232 = Or(Xor(b14,True),Xor(b78,True)) | |
| b233 = Or(Xor(b231,False),Xor(b232,True)) | |
| b234 = Xor(Xor(b15,False),Xor(b79,False)) | |
| b235 = Xor(Xor(b234,False),Xor(b233,False)) | |
| b236 = Or(Xor(b79,True),Xor(b233,True)) | |
| b237 = Or(Xor(b15,True),Xor(b233,True)) | |
| b238 = Or(Xor(b236,True),Xor(b237,True)) | |
| b239 = Or(Xor(b15,True),Xor(b79,True)) | |
| b240 = Or(Xor(b238,False),Xor(b239,True)) | |
| b241 = Xor(Xor(b16,False),Xor(b80,False)) | |
| b242 = Xor(Xor(b241,False),Xor(b240,False)) | |
| b243 = Or(Xor(b80,True),Xor(b240,True)) | |
| b244 = Or(Xor(b16,True),Xor(b240,True)) | |
| b245 = Or(Xor(b243,True),Xor(b244,True)) | |
| b246 = Or(Xor(b16,True),Xor(b80,True)) | |
| b247 = Or(Xor(b245,False),Xor(b246,True)) | |
| b248 = Xor(Xor(b17,False),Xor(b81,False)) | |
| b249 = Xor(Xor(b248,False),Xor(b247,False)) | |
| b250 = Or(Xor(b81,True),Xor(b247,True)) | |
| b251 = Or(Xor(b17,True),Xor(b247,True)) | |
| b252 = Or(Xor(b250,True),Xor(b251,True)) | |
| b253 = Or(Xor(b17,True),Xor(b81,True)) | |
| b254 = Or(Xor(b252,False),Xor(b253,True)) | |
| b255 = Xor(Xor(b18,False),Xor(b82,False)) | |
| b256 = Xor(Xor(b255,False),Xor(b254,False)) | |
| b257 = Or(Xor(b82,True),Xor(b254,True)) | |
| b258 = Or(Xor(b18,True),Xor(b254,True)) | |
| b259 = Or(Xor(b257,True),Xor(b258,True)) | |
| b260 = Or(Xor(b18,True),Xor(b82,True)) | |
| b261 = Or(Xor(b259,False),Xor(b260,True)) | |
| b262 = Xor(Xor(b19,False),Xor(b83,False)) | |
| b263 = Xor(Xor(b262,False),Xor(b261,False)) | |
| b264 = Or(Xor(b83,True),Xor(b261,True)) | |
| b265 = Or(Xor(b19,True),Xor(b261,True)) | |
| b266 = Or(Xor(b264,True),Xor(b265,True)) | |
| b267 = Or(Xor(b19,True),Xor(b83,True)) | |
| b268 = Or(Xor(b266,False),Xor(b267,True)) | |
| b269 = Xor(Xor(b20,False),Xor(b84,False)) | |
| b270 = Xor(Xor(b269,False),Xor(b268,False)) | |
| b271 = Or(Xor(b84,True),Xor(b268,True)) | |
| b272 = Or(Xor(b20,True),Xor(b268,True)) | |
| b273 = Or(Xor(b271,True),Xor(b272,True)) | |
| b274 = Or(Xor(b20,True),Xor(b84,True)) | |
| b275 = Or(Xor(b273,False),Xor(b274,True)) | |
| b276 = Xor(Xor(b21,False),Xor(b85,False)) | |
| b277 = Xor(Xor(b276,False),Xor(b275,False)) | |
| b278 = Or(Xor(b85,True),Xor(b275,True)) | |
| b279 = Or(Xor(b21,True),Xor(b275,True)) | |
| b280 = Or(Xor(b278,True),Xor(b279,True)) | |
| b281 = Or(Xor(b21,True),Xor(b85,True)) | |
| b282 = Or(Xor(b280,False),Xor(b281,True)) | |
| b283 = Xor(Xor(b22,False),Xor(b86,False)) | |
| b284 = Xor(Xor(b283,False),Xor(b282,False)) | |
| b285 = Or(Xor(b86,True),Xor(b282,True)) | |
| b286 = Or(Xor(b22,True),Xor(b282,True)) | |
| b287 = Or(Xor(b285,True),Xor(b286,True)) | |
| b288 = Or(Xor(b22,True),Xor(b86,True)) | |
| b289 = Or(Xor(b287,False),Xor(b288,True)) | |
| b290 = Xor(Xor(b23,False),Xor(b87,False)) | |
| b291 = Xor(Xor(b290,False),Xor(b289,False)) | |
| b292 = Or(Xor(b87,True),Xor(b289,True)) | |
| b293 = Or(Xor(b23,True),Xor(b289,True)) | |
| b294 = Or(Xor(b292,True),Xor(b293,True)) | |
| b295 = Or(Xor(b23,True),Xor(b87,True)) | |
| b296 = Or(Xor(b294,False),Xor(b295,True)) | |
| b297 = Xor(Xor(b24,False),Xor(b88,False)) | |
| b298 = Xor(Xor(b297,False),Xor(b296,False)) | |
| b299 = Or(Xor(b88,True),Xor(b296,True)) | |
| b300 = Or(Xor(b24,True),Xor(b296,True)) | |
| b301 = Or(Xor(b299,True),Xor(b300,True)) | |
| b302 = Or(Xor(b24,True),Xor(b88,True)) | |
| b303 = Or(Xor(b301,False),Xor(b302,True)) | |
| b304 = Xor(Xor(b25,False),Xor(b89,False)) | |
| b305 = Xor(Xor(b304,False),Xor(b303,False)) | |
| b306 = Or(Xor(b89,True),Xor(b303,True)) | |
| b307 = Or(Xor(b25,True),Xor(b303,True)) | |
| b308 = Or(Xor(b306,True),Xor(b307,True)) | |
| b309 = Or(Xor(b25,True),Xor(b89,True)) | |
| b310 = Or(Xor(b308,False),Xor(b309,True)) | |
| b311 = Xor(Xor(b26,False),Xor(b90,False)) | |
| b312 = Xor(Xor(b311,False),Xor(b310,False)) | |
| b313 = Or(Xor(b90,True),Xor(b310,True)) | |
| b314 = Or(Xor(b26,True),Xor(b310,True)) | |
| b315 = Or(Xor(b313,True),Xor(b314,True)) | |
| b316 = Or(Xor(b26,True),Xor(b90,True)) | |
| b317 = Or(Xor(b315,False),Xor(b316,True)) | |
| b318 = Xor(Xor(b27,False),Xor(b91,False)) | |
| b319 = Xor(Xor(b318,False),Xor(b317,False)) | |
| b320 = Or(Xor(b91,True),Xor(b317,True)) | |
| b321 = Or(Xor(b27,True),Xor(b317,True)) | |
| b322 = Or(Xor(b320,True),Xor(b321,True)) | |
| b323 = Or(Xor(b27,True),Xor(b91,True)) | |
| b324 = Or(Xor(b322,False),Xor(b323,True)) | |
| b325 = Xor(Xor(b28,False),Xor(b92,False)) | |
| b326 = Xor(Xor(b325,False),Xor(b324,False)) | |
| b327 = Or(Xor(b92,True),Xor(b324,True)) | |
| b328 = Or(Xor(b28,True),Xor(b324,True)) | |
| b329 = Or(Xor(b327,True),Xor(b328,True)) | |
| b330 = Or(Xor(b28,True),Xor(b92,True)) | |
| b331 = Or(Xor(b329,False),Xor(b330,True)) | |
| b332 = Xor(Xor(b29,False),Xor(b93,False)) | |
| b333 = Xor(Xor(b332,False),Xor(b331,False)) | |
| b334 = Or(Xor(b93,True),Xor(b331,True)) | |
| b335 = Or(Xor(b29,True),Xor(b331,True)) | |
| b336 = Or(Xor(b334,True),Xor(b335,True)) | |
| b337 = Or(Xor(b29,True),Xor(b93,True)) | |
| b338 = Or(Xor(b336,False),Xor(b337,True)) | |
| b339 = Xor(Xor(b30,False),Xor(b94,False)) | |
| b340 = Xor(Xor(b339,False),Xor(b338,False)) | |
| b341 = Or(Xor(b94,True),Xor(b338,True)) | |
| b342 = Or(Xor(b30,True),Xor(b338,True)) | |
| b343 = Or(Xor(b341,True),Xor(b342,True)) | |
| b344 = Or(Xor(b30,True),Xor(b94,True)) | |
| b345 = Or(Xor(b343,False),Xor(b344,True)) | |
| b346 = Xor(Xor(b31,False),Xor(b95,False)) | |
| b347 = Xor(Xor(b346,False),Xor(b345,False)) | |
| b348 = Or(Xor(b95,True),Xor(b345,True)) | |
| b349 = Or(Xor(b31,True),Xor(b345,True)) | |
| b350 = Or(Xor(b348,True),Xor(b349,True)) | |
| b351 = Or(Xor(b31,True),Xor(b95,True)) | |
| b352 = Or(Xor(b350,False),Xor(b351,True)) | |
| b353 = Xor(Xor(b32,False),Xor(b96,False)) | |
| b354 = Xor(Xor(b353,False),Xor(b352,False)) | |
| b355 = Or(Xor(b96,True),Xor(b352,True)) | |
| b356 = Or(Xor(b32,True),Xor(b352,True)) | |
| b357 = Or(Xor(b355,True),Xor(b356,True)) | |
| b358 = Or(Xor(b32,True),Xor(b96,True)) | |
| b359 = Or(Xor(b357,False),Xor(b358,True)) | |
| b360 = Xor(Xor(b33,False),Xor(b97,False)) | |
| b361 = Xor(Xor(b360,False),Xor(b359,False)) | |
| b362 = Or(Xor(b97,True),Xor(b359,True)) | |
| b363 = Or(Xor(b33,True),Xor(b359,True)) | |
| b364 = Or(Xor(b362,True),Xor(b363,True)) | |
| b365 = Or(Xor(b33,True),Xor(b97,True)) | |
| b366 = Or(Xor(b364,False),Xor(b365,True)) | |
| b367 = Xor(Xor(b34,False),Xor(b98,False)) | |
| b368 = Xor(Xor(b367,False),Xor(b366,False)) | |
| b369 = Or(Xor(b98,True),Xor(b366,True)) | |
| b370 = Or(Xor(b34,True),Xor(b366,True)) | |
| b371 = Or(Xor(b369,True),Xor(b370,True)) | |
| b372 = Or(Xor(b34,True),Xor(b98,True)) | |
| b373 = Or(Xor(b371,False),Xor(b372,True)) | |
| b374 = Xor(Xor(b35,False),Xor(b99,False)) | |
| b375 = Xor(Xor(b374,False),Xor(b373,False)) | |
| b376 = Or(Xor(b99,True),Xor(b373,True)) | |
| b377 = Or(Xor(b35,True),Xor(b373,True)) | |
| b378 = Or(Xor(b376,True),Xor(b377,True)) | |
| b379 = Or(Xor(b35,True),Xor(b99,True)) | |
| b380 = Or(Xor(b378,False),Xor(b379,True)) | |
| b381 = Xor(Xor(b36,False),Xor(b100,False)) | |
| b382 = Xor(Xor(b381,False),Xor(b380,False)) | |
| b383 = Or(Xor(b100,True),Xor(b380,True)) | |
| b384 = Or(Xor(b36,True),Xor(b380,True)) | |
| b385 = Or(Xor(b383,True),Xor(b384,True)) | |
| b386 = Or(Xor(b36,True),Xor(b100,True)) | |
| b387 = Or(Xor(b385,False),Xor(b386,True)) | |
| b388 = Xor(Xor(b37,False),Xor(b101,False)) | |
| b389 = Xor(Xor(b388,False),Xor(b387,False)) | |
| b390 = Or(Xor(b101,True),Xor(b387,True)) | |
| b391 = Or(Xor(b37,True),Xor(b387,True)) | |
| b392 = Or(Xor(b390,True),Xor(b391,True)) | |
| b393 = Or(Xor(b37,True),Xor(b101,True)) | |
| b394 = Or(Xor(b392,False),Xor(b393,True)) | |
| b395 = Xor(Xor(b38,False),Xor(b102,False)) | |
| b396 = Xor(Xor(b395,False),Xor(b394,False)) | |
| b397 = Or(Xor(b102,True),Xor(b394,True)) | |
| b398 = Or(Xor(b38,True),Xor(b394,True)) | |
| b399 = Or(Xor(b397,True),Xor(b398,True)) | |
| b400 = Or(Xor(b38,True),Xor(b102,True)) | |
| b401 = Or(Xor(b399,False),Xor(b400,True)) | |
| b402 = Xor(Xor(b39,False),Xor(b103,False)) | |
| b403 = Xor(Xor(b402,False),Xor(b401,False)) | |
| b404 = Or(Xor(b103,True),Xor(b401,True)) | |
| b405 = Or(Xor(b39,True),Xor(b401,True)) | |
| b406 = Or(Xor(b404,True),Xor(b405,True)) | |
| b407 = Or(Xor(b39,True),Xor(b103,True)) | |
| b408 = Or(Xor(b406,False),Xor(b407,True)) | |
| b409 = Xor(Xor(b40,False),Xor(b104,False)) | |
| b410 = Xor(Xor(b409,False),Xor(b408,False)) | |
| b411 = Or(Xor(b104,True),Xor(b408,True)) | |
| b412 = Or(Xor(b40,True),Xor(b408,True)) | |
| b413 = Or(Xor(b411,True),Xor(b412,True)) | |
| b414 = Or(Xor(b40,True),Xor(b104,True)) | |
| b415 = Or(Xor(b413,False),Xor(b414,True)) | |
| b416 = Xor(Xor(b41,False),Xor(b105,False)) | |
| b417 = Xor(Xor(b416,False),Xor(b415,False)) | |
| b418 = Or(Xor(b105,True),Xor(b415,True)) | |
| b419 = Or(Xor(b41,True),Xor(b415,True)) | |
| b420 = Or(Xor(b418,True),Xor(b419,True)) | |
| b421 = Or(Xor(b41,True),Xor(b105,True)) | |
| b422 = Or(Xor(b420,False),Xor(b421,True)) | |
| b423 = Xor(Xor(b42,False),Xor(b106,False)) | |
| b424 = Xor(Xor(b423,False),Xor(b422,False)) | |
| b425 = Or(Xor(b106,True),Xor(b422,True)) | |
| b426 = Or(Xor(b42,True),Xor(b422,True)) | |
| b427 = Or(Xor(b425,True),Xor(b426,True)) | |
| b428 = Or(Xor(b42,True),Xor(b106,True)) | |
| b429 = Or(Xor(b427,False),Xor(b428,True)) | |
| b430 = Xor(Xor(b43,False),Xor(b107,False)) | |
| b431 = Xor(Xor(b430,False),Xor(b429,False)) | |
| b432 = Or(Xor(b107,True),Xor(b429,True)) | |
| b433 = Or(Xor(b43,True),Xor(b429,True)) | |
| b434 = Or(Xor(b432,True),Xor(b433,True)) | |
| b435 = Or(Xor(b43,True),Xor(b107,True)) | |
| b436 = Or(Xor(b434,False),Xor(b435,True)) | |
| b437 = Xor(Xor(b44,False),Xor(b108,False)) | |
| b438 = Xor(Xor(b437,False),Xor(b436,False)) | |
| b439 = Or(Xor(b108,True),Xor(b436,True)) | |
| b440 = Or(Xor(b44,True),Xor(b436,True)) | |
| b441 = Or(Xor(b439,True),Xor(b440,True)) | |
| b442 = Or(Xor(b44,True),Xor(b108,True)) | |
| b443 = Or(Xor(b441,False),Xor(b442,True)) | |
| b444 = Xor(Xor(b45,False),Xor(b109,False)) | |
| b445 = Xor(Xor(b444,False),Xor(b443,False)) | |
| b446 = Or(Xor(b109,True),Xor(b443,True)) | |
| b447 = Or(Xor(b45,True),Xor(b443,True)) | |
| b448 = Or(Xor(b446,True),Xor(b447,True)) | |
| b449 = Or(Xor(b45,True),Xor(b109,True)) | |
| b450 = Or(Xor(b448,False),Xor(b449,True)) | |
| b451 = Xor(Xor(b46,False),Xor(b110,False)) | |
| b452 = Xor(Xor(b451,False),Xor(b450,False)) | |
| b453 = Or(Xor(b110,True),Xor(b450,True)) | |
| b454 = Or(Xor(b46,True),Xor(b450,True)) | |
| b455 = Or(Xor(b453,True),Xor(b454,True)) | |
| b456 = Or(Xor(b46,True),Xor(b110,True)) | |
| b457 = Or(Xor(b455,False),Xor(b456,True)) | |
| b458 = Xor(Xor(b47,False),Xor(b111,False)) | |
| b459 = Xor(Xor(b458,False),Xor(b457,False)) | |
| b460 = Or(Xor(b111,True),Xor(b457,True)) | |
| b461 = Or(Xor(b47,True),Xor(b457,True)) | |
| b462 = Or(Xor(b460,True),Xor(b461,True)) | |
| b463 = Or(Xor(b47,True),Xor(b111,True)) | |
| b464 = Or(Xor(b462,False),Xor(b463,True)) | |
| b465 = Xor(Xor(b48,False),Xor(b112,False)) | |
| b466 = Xor(Xor(b465,False),Xor(b464,False)) | |
| b467 = Or(Xor(b112,True),Xor(b464,True)) | |
| b468 = Or(Xor(b48,True),Xor(b464,True)) | |
| b469 = Or(Xor(b467,True),Xor(b468,True)) | |
| b470 = Or(Xor(b48,True),Xor(b112,True)) | |
| b471 = Or(Xor(b469,False),Xor(b470,True)) | |
| b472 = Xor(Xor(b49,False),Xor(b113,False)) | |
| b473 = Xor(Xor(b472,False),Xor(b471,False)) | |
| b474 = Or(Xor(b113,True),Xor(b471,True)) | |
| b475 = Or(Xor(b49,True),Xor(b471,True)) | |
| b476 = Or(Xor(b474,True),Xor(b475,True)) | |
| b477 = Or(Xor(b49,True),Xor(b113,True)) | |
| b478 = Or(Xor(b476,False),Xor(b477,True)) | |
| b479 = Xor(Xor(b50,False),Xor(b114,False)) | |
| b480 = Xor(Xor(b479,False),Xor(b478,False)) | |
| b481 = Or(Xor(b114,True),Xor(b478,True)) | |
| b482 = Or(Xor(b50,True),Xor(b478,True)) | |
| b483 = Or(Xor(b481,True),Xor(b482,True)) | |
| b484 = Or(Xor(b50,True),Xor(b114,True)) | |
| b485 = Or(Xor(b483,False),Xor(b484,True)) | |
| b486 = Xor(Xor(b51,False),Xor(b115,False)) | |
| b487 = Xor(Xor(b486,False),Xor(b485,False)) | |
| b488 = Or(Xor(b115,True),Xor(b485,True)) | |
| b489 = Or(Xor(b51,True),Xor(b485,True)) | |
| b490 = Or(Xor(b488,True),Xor(b489,True)) | |
| b491 = Or(Xor(b51,True),Xor(b115,True)) | |
| b492 = Or(Xor(b490,False),Xor(b491,True)) | |
| b493 = Xor(Xor(b52,False),Xor(b116,False)) | |
| b494 = Xor(Xor(b493,False),Xor(b492,False)) | |
| b495 = Or(Xor(b116,True),Xor(b492,True)) | |
| b496 = Or(Xor(b52,True),Xor(b492,True)) | |
| b497 = Or(Xor(b495,True),Xor(b496,True)) | |
| b498 = Or(Xor(b52,True),Xor(b116,True)) | |
| b499 = Or(Xor(b497,False),Xor(b498,True)) | |
| b500 = Xor(Xor(b53,False),Xor(b117,False)) | |
| b501 = Xor(Xor(b500,False),Xor(b499,False)) | |
| b502 = Or(Xor(b117,True),Xor(b499,True)) | |
| b503 = Or(Xor(b53,True),Xor(b499,True)) | |
| b504 = Or(Xor(b502,True),Xor(b503,True)) | |
| b505 = Or(Xor(b53,True),Xor(b117,True)) | |
| b506 = Or(Xor(b504,False),Xor(b505,True)) | |
| b507 = Xor(Xor(b54,False),Xor(b118,False)) | |
| b508 = Xor(Xor(b507,False),Xor(b506,False)) | |
| b509 = Or(Xor(b118,True),Xor(b506,True)) | |
| b510 = Or(Xor(b54,True),Xor(b506,True)) | |
| b511 = Or(Xor(b509,True),Xor(b510,True)) | |
| b512 = Or(Xor(b54,True),Xor(b118,True)) | |
| b513 = Or(Xor(b511,False),Xor(b512,True)) | |
| b514 = Xor(Xor(b55,False),Xor(b119,False)) | |
| b515 = Xor(Xor(b514,False),Xor(b513,False)) | |
| b516 = Or(Xor(b119,True),Xor(b513,True)) | |
| b517 = Or(Xor(b55,True),Xor(b513,True)) | |
| b518 = Or(Xor(b516,True),Xor(b517,True)) | |
| b519 = Or(Xor(b55,True),Xor(b119,True)) | |
| b520 = Or(Xor(b518,False),Xor(b519,True)) | |
| b521 = Xor(Xor(b56,False),Xor(b120,False)) | |
| b522 = Xor(Xor(b521,False),Xor(b520,False)) | |
| b523 = Or(Xor(b120,True),Xor(b520,True)) | |
| b524 = Or(Xor(b56,True),Xor(b520,True)) | |
| b525 = Or(Xor(b523,True),Xor(b524,True)) | |
| b526 = Or(Xor(b56,True),Xor(b120,True)) | |
| b527 = Or(Xor(b525,False),Xor(b526,True)) | |
| b528 = Xor(Xor(b57,False),Xor(b121,False)) | |
| b529 = Xor(Xor(b528,False),Xor(b527,False)) | |
| b530 = Or(Xor(b121,True),Xor(b527,True)) | |
| b531 = Or(Xor(b57,True),Xor(b527,True)) | |
| b532 = Or(Xor(b530,True),Xor(b531,True)) | |
| b533 = Or(Xor(b57,True),Xor(b121,True)) | |
| b534 = Or(Xor(b532,False),Xor(b533,True)) | |
| b535 = Xor(Xor(b58,False),Xor(b122,False)) | |
| b536 = Xor(Xor(b535,False),Xor(b534,False)) | |
| b537 = Or(Xor(b122,True),Xor(b534,True)) | |
| b538 = Or(Xor(b58,True),Xor(b534,True)) | |
| b539 = Or(Xor(b537,True),Xor(b538,True)) | |
| b540 = Or(Xor(b58,True),Xor(b122,True)) | |
| b541 = Or(Xor(b539,False),Xor(b540,True)) | |
| b542 = Xor(Xor(b59,False),Xor(b123,False)) | |
| b543 = Xor(Xor(b542,False),Xor(b541,False)) | |
| b544 = Or(Xor(b123,True),Xor(b541,True)) | |
| b545 = Or(Xor(b59,True),Xor(b541,True)) | |
| b546 = Or(Xor(b544,True),Xor(b545,True)) | |
| b547 = Or(Xor(b59,True),Xor(b123,True)) | |
| b548 = Or(Xor(b546,False),Xor(b547,True)) | |
| b549 = Xor(Xor(b60,False),Xor(b124,False)) | |
| b550 = Xor(Xor(b549,False),Xor(b548,False)) | |
| b551 = Or(Xor(b124,True),Xor(b548,True)) | |
| b552 = Or(Xor(b60,True),Xor(b548,True)) | |
| b553 = Or(Xor(b551,True),Xor(b552,True)) | |
| b554 = Or(Xor(b60,True),Xor(b124,True)) | |
| b555 = Or(Xor(b553,False),Xor(b554,True)) | |
| b556 = Xor(Xor(b61,False),Xor(b125,False)) | |
| b557 = Xor(Xor(b556,False),Xor(b555,False)) | |
| b558 = Or(Xor(b125,True),Xor(b555,True)) | |
| b559 = Or(Xor(b61,True),Xor(b555,True)) | |
| b560 = Or(Xor(b558,True),Xor(b559,True)) | |
| b561 = Or(Xor(b61,True),Xor(b125,True)) | |
| b562 = Or(Xor(b560,False),Xor(b561,True)) | |
| b563 = Xor(Xor(b62,False),Xor(b126,False)) | |
| b564 = Xor(Xor(b563,False),Xor(b562,False)) | |
| b565 = Or(Xor(b126,True),Xor(b562,True)) | |
| b566 = Or(Xor(b62,True),Xor(b562,True)) | |
| b567 = Or(Xor(b565,True),Xor(b566,True)) | |
| b568 = Or(Xor(b62,True),Xor(b126,True)) | |
| b569 = Or(Xor(b567,False),Xor(b568,True)) | |
| b570 = Xor(Xor(b63,False),Xor(b127,False)) | |
| b571 = Xor(Xor(b570,False),Xor(b569,False)) | |
| b572 = Xor(Xor(b0,False),Xor(b128,False)) | |
| b573 = Xor(Xor(b572,False),Xor(b128,True)) | |
| b574 = Or(Xor(b128,True),Xor(b128,False)) | |
| b575 = Or(Xor(b574,True),Xor(b132,True)) | |
| b576 = Or(Xor(b0,True),Xor(b128,True)) | |
| b577 = Or(Xor(b575,False),Xor(b576,True)) | |
| b578 = Xor(Xor(b1,False),Xor(b64,False)) | |
| b579 = Xor(Xor(b578,False),Xor(b577,False)) | |
| b580 = Or(Xor(b64,True),Xor(b577,True)) | |
| b581 = Or(Xor(b1,True),Xor(b577,True)) | |
| b582 = Or(Xor(b580,True),Xor(b581,True)) | |
| b583 = Or(Xor(b1,True),Xor(b64,True)) | |
| b584 = Or(Xor(b582,False),Xor(b583,True)) | |
| b585 = Xor(Xor(b2,False),Xor(b65,False)) | |
| b586 = Xor(Xor(b585,False),Xor(b584,False)) | |
| b587 = Or(Xor(b65,True),Xor(b584,True)) | |
| b588 = Or(Xor(b2,True),Xor(b584,True)) | |
| b589 = Or(Xor(b587,True),Xor(b588,True)) | |
| b590 = Or(Xor(b2,True),Xor(b65,True)) | |
| b591 = Or(Xor(b589,False),Xor(b590,True)) | |
| b592 = Xor(Xor(b3,False),Xor(b66,False)) | |
| b593 = Xor(Xor(b592,False),Xor(b591,False)) | |
| b594 = Or(Xor(b66,True),Xor(b591,True)) | |
| b595 = Or(Xor(b3,True),Xor(b591,True)) | |
| b596 = Or(Xor(b594,True),Xor(b595,True)) | |
| b597 = Or(Xor(b3,True),Xor(b66,True)) | |
| b598 = Or(Xor(b596,False),Xor(b597,True)) | |
| b599 = Xor(Xor(b4,False),Xor(b67,False)) | |
| b600 = Xor(Xor(b599,False),Xor(b598,False)) | |
| b601 = Or(Xor(b67,True),Xor(b598,True)) | |
| b602 = Or(Xor(b4,True),Xor(b598,True)) | |
| b603 = Or(Xor(b601,True),Xor(b602,True)) | |
| b604 = Or(Xor(b4,True),Xor(b67,True)) | |
| b605 = Or(Xor(b603,False),Xor(b604,True)) | |
| b606 = Xor(Xor(b5,False),Xor(b68,False)) | |
| b607 = Xor(Xor(b606,False),Xor(b605,False)) | |
| b608 = Or(Xor(b68,True),Xor(b605,True)) | |
| b609 = Or(Xor(b5,True),Xor(b605,True)) | |
| b610 = Or(Xor(b608,True),Xor(b609,True)) | |
| b611 = Or(Xor(b5,True),Xor(b68,True)) | |
| b612 = Or(Xor(b610,False),Xor(b611,True)) | |
| b613 = Xor(Xor(b6,False),Xor(b69,False)) | |
| b614 = Xor(Xor(b613,False),Xor(b612,False)) | |
| b615 = Or(Xor(b69,True),Xor(b612,True)) | |
| b616 = Or(Xor(b6,True),Xor(b612,True)) | |
| b617 = Or(Xor(b615,True),Xor(b616,True)) | |
| b618 = Or(Xor(b6,True),Xor(b69,True)) | |
| b619 = Or(Xor(b617,False),Xor(b618,True)) | |
| b620 = Xor(Xor(b7,False),Xor(b70,False)) | |
| b621 = Xor(Xor(b620,False),Xor(b619,False)) | |
| b622 = Or(Xor(b70,True),Xor(b619,True)) | |
| b623 = Or(Xor(b7,True),Xor(b619,True)) | |
| b624 = Or(Xor(b622,True),Xor(b623,True)) | |
| b625 = Or(Xor(b7,True),Xor(b70,True)) | |
| b626 = Or(Xor(b624,False),Xor(b625,True)) | |
| b627 = Xor(Xor(b8,False),Xor(b71,False)) | |
| b628 = Xor(Xor(b627,False),Xor(b626,False)) | |
| b629 = Or(Xor(b71,True),Xor(b626,True)) | |
| b630 = Or(Xor(b8,True),Xor(b626,True)) | |
| b631 = Or(Xor(b629,True),Xor(b630,True)) | |
| b632 = Or(Xor(b8,True),Xor(b71,True)) | |
| b633 = Or(Xor(b631,False),Xor(b632,True)) | |
| b634 = Xor(Xor(b9,False),Xor(b72,False)) | |
| b635 = Xor(Xor(b634,False),Xor(b633,False)) | |
| b636 = Or(Xor(b72,True),Xor(b633,True)) | |
| b637 = Or(Xor(b9,True),Xor(b633,True)) | |
| b638 = Or(Xor(b636,True),Xor(b637,True)) | |
| b639 = Or(Xor(b9,True),Xor(b72,True)) | |
| b640 = Or(Xor(b638,False),Xor(b639,True)) | |
| b641 = Xor(Xor(b10,False),Xor(b73,False)) | |
| b642 = Xor(Xor(b641,False),Xor(b640,False)) | |
| b643 = Or(Xor(b73,True),Xor(b640,True)) | |
| b644 = Or(Xor(b10,True),Xor(b640,True)) | |
| b645 = Or(Xor(b643,True),Xor(b644,True)) | |
| b646 = Or(Xor(b10,True),Xor(b73,True)) | |
| b647 = Or(Xor(b645,False),Xor(b646,True)) | |
| b648 = Xor(Xor(b11,False),Xor(b74,False)) | |
| b649 = Xor(Xor(b648,False),Xor(b647,False)) | |
| b650 = Or(Xor(b74,True),Xor(b647,True)) | |
| b651 = Or(Xor(b11,True),Xor(b647,True)) | |
| b652 = Or(Xor(b650,True),Xor(b651,True)) | |
| b653 = Or(Xor(b11,True),Xor(b74,True)) | |
| b654 = Or(Xor(b652,False),Xor(b653,True)) | |
| b655 = Xor(Xor(b12,False),Xor(b75,False)) | |
| b656 = Xor(Xor(b655,False),Xor(b654,False)) | |
| b657 = Or(Xor(b75,True),Xor(b654,True)) | |
| b658 = Or(Xor(b12,True),Xor(b654,True)) | |
| b659 = Or(Xor(b657,True),Xor(b658,True)) | |
| b660 = Or(Xor(b12,True),Xor(b75,True)) | |
| b661 = Or(Xor(b659,False),Xor(b660,True)) | |
| b662 = Xor(Xor(b13,False),Xor(b76,False)) | |
| b663 = Xor(Xor(b662,False),Xor(b661,False)) | |
| b664 = Or(Xor(b76,True),Xor(b661,True)) | |
| b665 = Or(Xor(b13,True),Xor(b661,True)) | |
| b666 = Or(Xor(b664,True),Xor(b665,True)) | |
| b667 = Or(Xor(b13,True),Xor(b76,True)) | |
| b668 = Or(Xor(b666,False),Xor(b667,True)) | |
| b669 = Xor(Xor(b14,False),Xor(b77,False)) | |
| b670 = Xor(Xor(b669,False),Xor(b668,False)) | |
| b671 = Or(Xor(b77,True),Xor(b668,True)) | |
| b672 = Or(Xor(b14,True),Xor(b668,True)) | |
| b673 = Or(Xor(b671,True),Xor(b672,True)) | |
| b674 = Or(Xor(b14,True),Xor(b77,True)) | |
| b675 = Or(Xor(b673,False),Xor(b674,True)) | |
| b676 = Xor(Xor(b15,False),Xor(b78,False)) | |
| b677 = Xor(Xor(b676,False),Xor(b675,False)) | |
| b678 = Or(Xor(b78,True),Xor(b675,True)) | |
| b679 = Or(Xor(b15,True),Xor(b675,True)) | |
| b680 = Or(Xor(b678,True),Xor(b679,True)) | |
| b681 = Or(Xor(b15,True),Xor(b78,True)) | |
| b682 = Or(Xor(b680,False),Xor(b681,True)) | |
| b683 = Xor(Xor(b16,False),Xor(b79,False)) | |
| b684 = Xor(Xor(b683,False),Xor(b682,False)) | |
| b685 = Or(Xor(b79,True),Xor(b682,True)) | |
| b686 = Or(Xor(b16,True),Xor(b682,True)) | |
| b687 = Or(Xor(b685,True),Xor(b686,True)) | |
| b688 = Or(Xor(b16,True),Xor(b79,True)) | |
| b689 = Or(Xor(b687,False),Xor(b688,True)) | |
| b690 = Xor(Xor(b17,False),Xor(b80,False)) | |
| b691 = Xor(Xor(b690,False),Xor(b689,False)) | |
| b692 = Or(Xor(b80,True),Xor(b689,True)) | |
| b693 = Or(Xor(b17,True),Xor(b689,True)) | |
| b694 = Or(Xor(b692,True),Xor(b693,True)) | |
| b695 = Or(Xor(b17,True),Xor(b80,True)) | |
| b696 = Or(Xor(b694,False),Xor(b695,True)) | |
| b697 = Xor(Xor(b18,False),Xor(b81,False)) | |
| b698 = Xor(Xor(b697,False),Xor(b696,False)) | |
| b699 = Or(Xor(b81,True),Xor(b696,True)) | |
| b700 = Or(Xor(b18,True),Xor(b696,True)) | |
| b701 = Or(Xor(b699,True),Xor(b700,True)) | |
| b702 = Or(Xor(b18,True),Xor(b81,True)) | |
| b703 = Or(Xor(b701,False),Xor(b702,True)) | |
| b704 = Xor(Xor(b19,False),Xor(b82,False)) | |
| b705 = Xor(Xor(b704,False),Xor(b703,False)) | |
| b706 = Or(Xor(b82,True),Xor(b703,True)) | |
| b707 = Or(Xor(b19,True),Xor(b703,True)) | |
| b708 = Or(Xor(b706,True),Xor(b707,True)) | |
| b709 = Or(Xor(b19,True),Xor(b82,True)) | |
| b710 = Or(Xor(b708,False),Xor(b709,True)) | |
| b711 = Xor(Xor(b20,False),Xor(b83,False)) | |
| b712 = Xor(Xor(b711,False),Xor(b710,False)) | |
| b713 = Or(Xor(b83,True),Xor(b710,True)) | |
| b714 = Or(Xor(b20,True),Xor(b710,True)) | |
| b715 = Or(Xor(b713,True),Xor(b714,True)) | |
| b716 = Or(Xor(b20,True),Xor(b83,True)) | |
| b717 = Or(Xor(b715,False),Xor(b716,True)) | |
| b718 = Xor(Xor(b21,False),Xor(b84,False)) | |
| b719 = Xor(Xor(b718,False),Xor(b717,False)) | |
| b720 = Or(Xor(b84,True),Xor(b717,True)) | |
| b721 = Or(Xor(b21,True),Xor(b717,True)) | |
| b722 = Or(Xor(b720,True),Xor(b721,True)) | |
| b723 = Or(Xor(b21,True),Xor(b84,True)) | |
| b724 = Or(Xor(b722,False),Xor(b723,True)) | |
| b725 = Xor(Xor(b22,False),Xor(b85,False)) | |
| b726 = Xor(Xor(b725,False),Xor(b724,False)) | |
| b727 = Or(Xor(b85,True),Xor(b724,True)) | |
| b728 = Or(Xor(b22,True),Xor(b724,True)) | |
| b729 = Or(Xor(b727,True),Xor(b728,True)) | |
| b730 = Or(Xor(b22,True),Xor(b85,True)) | |
| b731 = Or(Xor(b729,False),Xor(b730,True)) | |
| b732 = Xor(Xor(b23,False),Xor(b86,False)) | |
| b733 = Xor(Xor(b732,False),Xor(b731,False)) | |
| b734 = Or(Xor(b86,True),Xor(b731,True)) | |
| b735 = Or(Xor(b23,True),Xor(b731,True)) | |
| b736 = Or(Xor(b734,True),Xor(b735,True)) | |
| b737 = Or(Xor(b23,True),Xor(b86,True)) | |
| b738 = Or(Xor(b736,False),Xor(b737,True)) | |
| b739 = Xor(Xor(b24,False),Xor(b87,False)) | |
| b740 = Xor(Xor(b739,False),Xor(b738,False)) | |
| b741 = Or(Xor(b87,True),Xor(b738,True)) | |
| b742 = Or(Xor(b24,True),Xor(b738,True)) | |
| b743 = Or(Xor(b741,True),Xor(b742,True)) | |
| b744 = Or(Xor(b24,True),Xor(b87,True)) | |
| b745 = Or(Xor(b743,False),Xor(b744,True)) | |
| b746 = Xor(Xor(b25,False),Xor(b88,False)) | |
| b747 = Xor(Xor(b746,False),Xor(b745,False)) | |
| b748 = Or(Xor(b88,True),Xor(b745,True)) | |
| b749 = Or(Xor(b25,True),Xor(b745,True)) | |
| b750 = Or(Xor(b748,True),Xor(b749,True)) | |
| b751 = Or(Xor(b25,True),Xor(b88,True)) | |
| b752 = Or(Xor(b750,False),Xor(b751,True)) | |
| b753 = Xor(Xor(b26,False),Xor(b89,False)) | |
| b754 = Xor(Xor(b753,False),Xor(b752,False)) | |
| b755 = Or(Xor(b89,True),Xor(b752,True)) | |
| b756 = Or(Xor(b26,True),Xor(b752,True)) | |
| b757 = Or(Xor(b755,True),Xor(b756,True)) | |
| b758 = Or(Xor(b26,True),Xor(b89,True)) | |
| b759 = Or(Xor(b757,False),Xor(b758,True)) | |
| b760 = Xor(Xor(b27,False),Xor(b90,False)) | |
| b761 = Xor(Xor(b760,False),Xor(b759,False)) | |
| b762 = Or(Xor(b90,True),Xor(b759,True)) | |
| b763 = Or(Xor(b27,True),Xor(b759,True)) | |
| b764 = Or(Xor(b762,True),Xor(b763,True)) | |
| b765 = Or(Xor(b27,True),Xor(b90,True)) | |
| b766 = Or(Xor(b764,False),Xor(b765,True)) | |
| b767 = Xor(Xor(b28,False),Xor(b91,False)) | |
| b768 = Xor(Xor(b767,False),Xor(b766,False)) | |
| b769 = Or(Xor(b91,True),Xor(b766,True)) | |
| b770 = Or(Xor(b28,True),Xor(b766,True)) | |
| b771 = Or(Xor(b769,True),Xor(b770,True)) | |
| b772 = Or(Xor(b28,True),Xor(b91,True)) | |
| b773 = Or(Xor(b771,False),Xor(b772,True)) | |
| b774 = Xor(Xor(b29,False),Xor(b92,False)) | |
| b775 = Xor(Xor(b774,False),Xor(b773,False)) | |
| b776 = Or(Xor(b92,True),Xor(b773,True)) | |
| b777 = Or(Xor(b29,True),Xor(b773,True)) | |
| b778 = Or(Xor(b776,True),Xor(b777,True)) | |
| b779 = Or(Xor(b29,True),Xor(b92,True)) | |
| b780 = Or(Xor(b778,False),Xor(b779,True)) | |
| b781 = Xor(Xor(b30,False),Xor(b93,False)) | |
| b782 = Xor(Xor(b781,False),Xor(b780,False)) | |
| b783 = Or(Xor(b93,True),Xor(b780,True)) | |
| b784 = Or(Xor(b30,True),Xor(b780,True)) | |
| b785 = Or(Xor(b783,True),Xor(b784,True)) | |
| b786 = Or(Xor(b30,True),Xor(b93,True)) | |
| b787 = Or(Xor(b785,False),Xor(b786,True)) | |
| b788 = Xor(Xor(b31,False),Xor(b94,False)) | |
| b789 = Xor(Xor(b788,False),Xor(b787,False)) | |
| b790 = Or(Xor(b94,True),Xor(b787,True)) | |
| b791 = Or(Xor(b31,True),Xor(b787,True)) | |
| b792 = Or(Xor(b790,True),Xor(b791,True)) | |
| b793 = Or(Xor(b31,True),Xor(b94,True)) | |
| b794 = Or(Xor(b792,False),Xor(b793,True)) | |
| b795 = Xor(Xor(b32,False),Xor(b95,False)) | |
| b796 = Xor(Xor(b795,False),Xor(b794,False)) | |
| b797 = Or(Xor(b95,True),Xor(b794,True)) | |
| b798 = Or(Xor(b32,True),Xor(b794,True)) | |
| b799 = Or(Xor(b797,True),Xor(b798,True)) | |
| b800 = Or(Xor(b32,True),Xor(b95,True)) | |
| b801 = Or(Xor(b799,False),Xor(b800,True)) | |
| b802 = Xor(Xor(b33,False),Xor(b96,False)) | |
| b803 = Xor(Xor(b802,False),Xor(b801,False)) | |
| b804 = Or(Xor(b96,True),Xor(b801,True)) | |
| b805 = Or(Xor(b33,True),Xor(b801,True)) | |
| b806 = Or(Xor(b804,True),Xor(b805,True)) | |
| b807 = Or(Xor(b33,True),Xor(b96,True)) | |
| b808 = Or(Xor(b806,False),Xor(b807,True)) | |
| b809 = Xor(Xor(b34,False),Xor(b97,False)) | |
| b810 = Xor(Xor(b809,False),Xor(b808,False)) | |
| b811 = Or(Xor(b97,True),Xor(b808,True)) | |
| b812 = Or(Xor(b34,True),Xor(b808,True)) | |
| b813 = Or(Xor(b811,True),Xor(b812,True)) | |
| b814 = Or(Xor(b34,True),Xor(b97,True)) | |
| b815 = Or(Xor(b813,False),Xor(b814,True)) | |
| b816 = Xor(Xor(b35,False),Xor(b98,False)) | |
| b817 = Xor(Xor(b816,False),Xor(b815,False)) | |
| b818 = Or(Xor(b98,True),Xor(b815,True)) | |
| b819 = Or(Xor(b35,True),Xor(b815,True)) | |
| b820 = Or(Xor(b818,True),Xor(b819,True)) | |
| b821 = Or(Xor(b35,True),Xor(b98,True)) | |
| b822 = Or(Xor(b820,False),Xor(b821,True)) | |
| b823 = Xor(Xor(b36,False),Xor(b99,False)) | |
| b824 = Xor(Xor(b823,False),Xor(b822,False)) | |
| b825 = Or(Xor(b99,True),Xor(b822,True)) | |
| b826 = Or(Xor(b36,True),Xor(b822,True)) | |
| b827 = Or(Xor(b825,True),Xor(b826,True)) | |
| b828 = Or(Xor(b36,True),Xor(b99,True)) | |
| b829 = Or(Xor(b827,False),Xor(b828,True)) | |
| b830 = Xor(Xor(b37,False),Xor(b100,False)) | |
| b831 = Xor(Xor(b830,False),Xor(b829,False)) | |
| b832 = Or(Xor(b100,True),Xor(b829,True)) | |
| b833 = Or(Xor(b37,True),Xor(b829,True)) | |
| b834 = Or(Xor(b832,True),Xor(b833,True)) | |
| b835 = Or(Xor(b37,True),Xor(b100,True)) | |
| b836 = Or(Xor(b834,False),Xor(b835,True)) | |
| b837 = Xor(Xor(b38,False),Xor(b101,False)) | |
| b838 = Xor(Xor(b837,False),Xor(b836,False)) | |
| b839 = Or(Xor(b101,True),Xor(b836,True)) | |
| b840 = Or(Xor(b38,True),Xor(b836,True)) | |
| b841 = Or(Xor(b839,True),Xor(b840,True)) | |
| b842 = Or(Xor(b38,True),Xor(b101,True)) | |
| b843 = Or(Xor(b841,False),Xor(b842,True)) | |
| b844 = Xor(Xor(b39,False),Xor(b102,False)) | |
| b845 = Xor(Xor(b844,False),Xor(b843,False)) | |
| b846 = Or(Xor(b102,True),Xor(b843,True)) | |
| b847 = Or(Xor(b39,True),Xor(b843,True)) | |
| b848 = Or(Xor(b846,True),Xor(b847,True)) | |
| b849 = Or(Xor(b39,True),Xor(b102,True)) | |
| b850 = Or(Xor(b848,False),Xor(b849,True)) | |
| b851 = Xor(Xor(b40,False),Xor(b103,False)) | |
| b852 = Xor(Xor(b851,False),Xor(b850,False)) | |
| b853 = Or(Xor(b103,True),Xor(b850,True)) | |
| b854 = Or(Xor(b40,True),Xor(b850,True)) | |
| b855 = Or(Xor(b853,True),Xor(b854,True)) | |
| b856 = Or(Xor(b40,True),Xor(b103,True)) | |
| b857 = Or(Xor(b855,False),Xor(b856,True)) | |
| b858 = Xor(Xor(b41,False),Xor(b104,False)) | |
| b859 = Xor(Xor(b858,False),Xor(b857,False)) | |
| b860 = Or(Xor(b104,True),Xor(b857,True)) | |
| b861 = Or(Xor(b41,True),Xor(b857,True)) | |
| b862 = Or(Xor(b860,True),Xor(b861,True)) | |
| b863 = Or(Xor(b41,True),Xor(b104,True)) | |
| b864 = Or(Xor(b862,False),Xor(b863,True)) | |
| b865 = Xor(Xor(b42,False),Xor(b105,False)) | |
| b866 = Xor(Xor(b865,False),Xor(b864,False)) | |
| b867 = Or(Xor(b105,True),Xor(b864,True)) | |
| b868 = Or(Xor(b42,True),Xor(b864,True)) | |
| b869 = Or(Xor(b867,True),Xor(b868,True)) | |
| b870 = Or(Xor(b42,True),Xor(b105,True)) | |
| b871 = Or(Xor(b869,False),Xor(b870,True)) | |
| b872 = Xor(Xor(b43,False),Xor(b106,False)) | |
| b873 = Xor(Xor(b872,False),Xor(b871,False)) | |
| b874 = Or(Xor(b106,True),Xor(b871,True)) | |
| b875 = Or(Xor(b43,True),Xor(b871,True)) | |
| b876 = Or(Xor(b874,True),Xor(b875,True)) | |
| b877 = Or(Xor(b43,True),Xor(b106,True)) | |
| b878 = Or(Xor(b876,False),Xor(b877,True)) | |
| b879 = Xor(Xor(b44,False),Xor(b107,False)) | |
| b880 = Xor(Xor(b879,False),Xor(b878,False)) | |
| b881 = Or(Xor(b107,True),Xor(b878,True)) | |
| b882 = Or(Xor(b44,True),Xor(b878,True)) | |
| b883 = Or(Xor(b881,True),Xor(b882,True)) | |
| b884 = Or(Xor(b44,True),Xor(b107,True)) | |
| b885 = Or(Xor(b883,False),Xor(b884,True)) | |
| b886 = Xor(Xor(b45,False),Xor(b108,False)) | |
| b887 = Xor(Xor(b886,False),Xor(b885,False)) | |
| b888 = Or(Xor(b108,True),Xor(b885,True)) | |
| b889 = Or(Xor(b45,True),Xor(b885,True)) | |
| b890 = Or(Xor(b888,True),Xor(b889,True)) | |
| b891 = Or(Xor(b45,True),Xor(b108,True)) | |
| b892 = Or(Xor(b890,False),Xor(b891,True)) | |
| b893 = Xor(Xor(b46,False),Xor(b109,False)) | |
| b894 = Xor(Xor(b893,False),Xor(b892,False)) | |
| b895 = Or(Xor(b109,True),Xor(b892,True)) | |
| b896 = Or(Xor(b46,True),Xor(b892,True)) | |
| b897 = Or(Xor(b895,True),Xor(b896,True)) | |
| b898 = Or(Xor(b46,True),Xor(b109,True)) | |
| b899 = Or(Xor(b897,False),Xor(b898,True)) | |
| b900 = Xor(Xor(b47,False),Xor(b110,False)) | |
| b901 = Xor(Xor(b900,False),Xor(b899,False)) | |
| b902 = Or(Xor(b110,True),Xor(b899,True)) | |
| b903 = Or(Xor(b47,True),Xor(b899,True)) | |
| b904 = Or(Xor(b902,True),Xor(b903,True)) | |
| b905 = Or(Xor(b47,True),Xor(b110,True)) | |
| b906 = Or(Xor(b904,False),Xor(b905,True)) | |
| b907 = Xor(Xor(b48,False),Xor(b111,False)) | |
| b908 = Xor(Xor(b907,False),Xor(b906,False)) | |
| b909 = Or(Xor(b111,True),Xor(b906,True)) | |
| b910 = Or(Xor(b48,True),Xor(b906,True)) | |
| b911 = Or(Xor(b909,True),Xor(b910,True)) | |
| b912 = Or(Xor(b48,True),Xor(b111,True)) | |
| b913 = Or(Xor(b911,False),Xor(b912,True)) | |
| b914 = Xor(Xor(b49,False),Xor(b112,False)) | |
| b915 = Xor(Xor(b914,False),Xor(b913,False)) | |
| b916 = Or(Xor(b112,True),Xor(b913,True)) | |
| b917 = Or(Xor(b49,True),Xor(b913,True)) | |
| b918 = Or(Xor(b916,True),Xor(b917,True)) | |
| b919 = Or(Xor(b49,True),Xor(b112,True)) | |
| b920 = Or(Xor(b918,False),Xor(b919,True)) | |
| b921 = Xor(Xor(b50,False),Xor(b113,False)) | |
| b922 = Xor(Xor(b921,False),Xor(b920,False)) | |
| b923 = Or(Xor(b113,True),Xor(b920,True)) | |
| b924 = Or(Xor(b50,True),Xor(b920,True)) | |
| b925 = Or(Xor(b923,True),Xor(b924,True)) | |
| b926 = Or(Xor(b50,True),Xor(b113,True)) | |
| b927 = Or(Xor(b925,False),Xor(b926,True)) | |
| b928 = Xor(Xor(b51,False),Xor(b114,False)) | |
| b929 = Xor(Xor(b928,False),Xor(b927,False)) | |
| b930 = Or(Xor(b114,True),Xor(b927,True)) | |
| b931 = Or(Xor(b51,True),Xor(b927,True)) | |
| b932 = Or(Xor(b930,True),Xor(b931,True)) | |
| b933 = Or(Xor(b51,True),Xor(b114,True)) | |
| b934 = Or(Xor(b932,False),Xor(b933,True)) | |
| b935 = Xor(Xor(b52,False),Xor(b115,False)) | |
| b936 = Xor(Xor(b935,False),Xor(b934,False)) | |
| b937 = Or(Xor(b115,True),Xor(b934,True)) | |
| b938 = Or(Xor(b52,True),Xor(b934,True)) | |
| b939 = Or(Xor(b937,True),Xor(b938,True)) | |
| b940 = Or(Xor(b52,True),Xor(b115,True)) | |
| b941 = Or(Xor(b939,False),Xor(b940,True)) | |
| b942 = Xor(Xor(b53,False),Xor(b116,False)) | |
| b943 = Xor(Xor(b942,False),Xor(b941,False)) | |
| b944 = Or(Xor(b116,True),Xor(b941,True)) | |
| b945 = Or(Xor(b53,True),Xor(b941,True)) | |
| b946 = Or(Xor(b944,True),Xor(b945,True)) | |
| b947 = Or(Xor(b53,True),Xor(b116,True)) | |
| b948 = Or(Xor(b946,False),Xor(b947,True)) | |
| b949 = Xor(Xor(b54,False),Xor(b117,False)) | |
| b950 = Xor(Xor(b949,False),Xor(b948,False)) | |
| b951 = Or(Xor(b117,True),Xor(b948,True)) | |
| b952 = Or(Xor(b54,True),Xor(b948,True)) | |
| b953 = Or(Xor(b951,True),Xor(b952,True)) | |
| b954 = Or(Xor(b54,True),Xor(b117,True)) | |
| b955 = Or(Xor(b953,False),Xor(b954,True)) | |
| b956 = Xor(Xor(b55,False),Xor(b118,False)) | |
| b957 = Xor(Xor(b956,False),Xor(b955,False)) | |
| b958 = Or(Xor(b118,True),Xor(b955,True)) | |
| b959 = Or(Xor(b55,True),Xor(b955,True)) | |
| b960 = Or(Xor(b958,True),Xor(b959,True)) | |
| b961 = Or(Xor(b55,True),Xor(b118,True)) | |
| b962 = Or(Xor(b960,False),Xor(b961,True)) | |
| b963 = Xor(Xor(b56,False),Xor(b119,False)) | |
| b964 = Xor(Xor(b963,False),Xor(b962,False)) | |
| b965 = Or(Xor(b119,True),Xor(b962,True)) | |
| b966 = Or(Xor(b56,True),Xor(b962,True)) | |
| b967 = Or(Xor(b965,True),Xor(b966,True)) | |
| b968 = Or(Xor(b56,True),Xor(b119,True)) | |
| b969 = Or(Xor(b967,False),Xor(b968,True)) | |
| b970 = Xor(Xor(b57,False),Xor(b120,False)) | |
| b971 = Xor(Xor(b970,False),Xor(b969,False)) | |
| b972 = Or(Xor(b120,True),Xor(b969,True)) | |
| b973 = Or(Xor(b57,True),Xor(b969,True)) | |
| b974 = Or(Xor(b972,True),Xor(b973,True)) | |
| b975 = Or(Xor(b57,True),Xor(b120,True)) | |
| b976 = Or(Xor(b974,False),Xor(b975,True)) | |
| b977 = Xor(Xor(b58,False),Xor(b121,False)) | |
| b978 = Xor(Xor(b977,False),Xor(b976,False)) | |
| b979 = Or(Xor(b121,True),Xor(b976,True)) | |
| b980 = Or(Xor(b58,True),Xor(b976,True)) | |
| b981 = Or(Xor(b979,True),Xor(b980,True)) | |
| b982 = Or(Xor(b58,True),Xor(b121,True)) | |
| b983 = Or(Xor(b981,False),Xor(b982,True)) | |
| b984 = Xor(Xor(b59,False),Xor(b122,False)) | |
| b985 = Xor(Xor(b984,False),Xor(b983,False)) | |
| b986 = Or(Xor(b122,True),Xor(b983,True)) | |
| b987 = Or(Xor(b59,True),Xor(b983,True)) | |
| b988 = Or(Xor(b986,True),Xor(b987,True)) | |
| b989 = Or(Xor(b59,True),Xor(b122,True)) | |
| b990 = Or(Xor(b988,False),Xor(b989,True)) | |
| b991 = Xor(Xor(b60,False),Xor(b123,False)) | |
| b992 = Xor(Xor(b991,False),Xor(b990,False)) | |
| b993 = Or(Xor(b123,True),Xor(b990,True)) | |
| b994 = Or(Xor(b60,True),Xor(b990,True)) | |
| b995 = Or(Xor(b993,True),Xor(b994,True)) | |
| b996 = Or(Xor(b60,True),Xor(b123,True)) | |
| b997 = Or(Xor(b995,False),Xor(b996,True)) | |
| b998 = Xor(Xor(b61,False),Xor(b124,False)) | |
| b999 = Xor(Xor(b998,False),Xor(b997,False)) | |
| b1000 = Or(Xor(b124,True),Xor(b997,True)) | |
| b1001 = Or(Xor(b61,True),Xor(b997,True)) | |
| b1002 = Or(Xor(b1000,True),Xor(b1001,True)) | |
| b1003 = Or(Xor(b61,True),Xor(b124,True)) | |
| b1004 = Or(Xor(b1002,False),Xor(b1003,True)) | |
| b1005 = Xor(Xor(b62,False),Xor(b125,False)) | |
| b1006 = Xor(Xor(b1005,False),Xor(b1004,False)) | |
| b1007 = Or(Xor(b125,True),Xor(b1004,True)) | |
| b1008 = Or(Xor(b62,True),Xor(b1004,True)) | |
| b1009 = Or(Xor(b1007,True),Xor(b1008,True)) | |
| b1010 = Or(Xor(b62,True),Xor(b125,True)) | |
| b1011 = Or(Xor(b1009,False),Xor(b1010,True)) | |
| b1012 = Xor(Xor(b63,False),Xor(b126,False)) | |
| b1013 = Xor(Xor(b1012,False),Xor(b1011,False)) | |
| b1014 = Or(Xor(b130,False),Xor(b137,False)) | |
| b1015 = Or(Xor(b144,True),Xor(b151,False)) | |
| b1016 = Or(Xor(b1014,False),Xor(b1015,False)) | |
| b1017 = Or(Xor(b158,False),Xor(b165,True)) | |
| b1018 = Or(Xor(b172,False),Xor(b179,False)) | |
| b1019 = Or(Xor(b1017,False),Xor(b1018,False)) | |
| b1020 = Or(Xor(b1016,False),Xor(b1019,False)) | |
| b1021 = Or(Xor(b186,True),Xor(b193,False)) | |
| b1022 = Or(Xor(b200,False),Xor(b207,True)) | |
| b1023 = Or(Xor(b1021,False),Xor(b1022,False)) | |
| b1024 = Or(Xor(b214,True),Xor(b221,True)) | |
| b1025 = Or(Xor(b228,True),Xor(b235,False)) | |
| b1026 = Or(Xor(b1024,False),Xor(b1025,False)) | |
| b1027 = Or(Xor(b1023,False),Xor(b1026,False)) | |
| b1028 = Or(Xor(b1020,False),Xor(b1027,False)) | |
| b1029 = Or(Xor(b242,True),Xor(b249,False)) | |
| b1030 = Or(Xor(b256,False),Xor(b263,True)) | |
| b1031 = Or(Xor(b1029,False),Xor(b1030,False)) | |
| b1032 = Or(Xor(b270,False),Xor(b277,False)) | |
| b1033 = Or(Xor(b284,False),Xor(b291,False)) | |
| b1034 = Or(Xor(b1032,False),Xor(b1033,False)) | |
| b1035 = Or(Xor(b1031,False),Xor(b1034,False)) | |
| b1036 = Or(Xor(b298,True),Xor(b305,False)) | |
| b1037 = Or(Xor(b312,True),Xor(b319,False)) | |
| b1038 = Or(Xor(b1036,False),Xor(b1037,False)) | |
| b1039 = Or(Xor(b326,False),Xor(b333,True)) | |
| b1040 = Or(Xor(b340,True),Xor(b347,False)) | |
| b1041 = Or(Xor(b1039,False),Xor(b1040,False)) | |
| b1042 = Or(Xor(b1038,False),Xor(b1041,False)) | |
| b1043 = Or(Xor(b1035,False),Xor(b1042,False)) | |
| b1044 = Or(Xor(b1028,False),Xor(b1043,False)) | |
| b1045 = Or(Xor(b354,True),Xor(b361,False)) | |
| b1046 = Or(Xor(b368,False),Xor(b375,True)) | |
| b1047 = Or(Xor(b1045,False),Xor(b1046,False)) | |
| b1048 = Or(Xor(b382,True),Xor(b389,True)) | |
| b1049 = Or(Xor(b396,True),Xor(b403,True)) | |
| b1050 = Or(Xor(b1048,False),Xor(b1049,False)) | |
| b1051 = Or(Xor(b1047,False),Xor(b1050,False)) | |
| b1052 = Or(Xor(b410,False),Xor(b417,True)) | |
| b1053 = Or(Xor(b424,True),Xor(b431,False)) | |
| b1054 = Or(Xor(b1052,False),Xor(b1053,False)) | |
| b1055 = Or(Xor(b438,True),Xor(b445,False)) | |
| b1056 = Or(Xor(b452,False),Xor(b459,False)) | |
| b1057 = Or(Xor(b1055,False),Xor(b1056,False)) | |
| b1058 = Or(Xor(b1054,False),Xor(b1057,False)) | |
| b1059 = Or(Xor(b1051,False),Xor(b1058,False)) | |
| b1060 = Or(Xor(b466,True),Xor(b473,True)) | |
| b1061 = Or(Xor(b480,False),Xor(b487,True)) | |
| b1062 = Or(Xor(b1060,False),Xor(b1061,False)) | |
| b1063 = Or(Xor(b494,False),Xor(b501,False)) | |
| b1064 = Or(Xor(b508,False),Xor(b515,False)) | |
| b1065 = Or(Xor(b1063,False),Xor(b1064,False)) | |
| b1066 = Or(Xor(b1062,False),Xor(b1065,False)) | |
| b1067 = Or(Xor(b522,False),Xor(b529,False)) | |
| b1068 = Or(Xor(b536,True),Xor(b543,True)) | |
| b1069 = Or(Xor(b1067,False),Xor(b1068,False)) | |
| b1070 = Or(Xor(b550,True),Xor(b557,True)) | |
| b1071 = Or(Xor(b564,False),Xor(b571,False)) | |
| b1072 = Or(Xor(b1070,False),Xor(b1071,False)) | |
| b1073 = Or(Xor(b1069,False),Xor(b1072,False)) | |
| b1074 = Or(Xor(b1066,False),Xor(b1073,False)) | |
| b1075 = Or(Xor(b1059,False),Xor(b1074,False)) | |
| b1076 = Or(Xor(b1044,False),Xor(b1075,False)) | |
| b1077 = Or(Xor(b573,False),Xor(b579,False)) | |
| b1078 = Or(Xor(b586,True),Xor(b593,True)) | |
| b1079 = Or(Xor(b1077,False),Xor(b1078,False)) | |
| b1080 = Or(Xor(b600,True),Xor(b607,True)) | |
| b1081 = Or(Xor(b614,True),Xor(b621,False)) | |
| b1082 = Or(Xor(b1080,False),Xor(b1081,False)) | |
| b1083 = Or(Xor(b1079,False),Xor(b1082,False)) | |
| b1084 = Or(Xor(b628,True),Xor(b635,True)) | |
| b1085 = Or(Xor(b642,True),Xor(b649,True)) | |
| b1086 = Or(Xor(b1084,False),Xor(b1085,False)) | |
| b1087 = Or(Xor(b656,True),Xor(b663,True)) | |
| b1088 = Or(Xor(b670,False),Xor(b677,True)) | |
| b1089 = Or(Xor(b1087,False),Xor(b1088,False)) | |
| b1090 = Or(Xor(b1086,False),Xor(b1089,False)) | |
| b1091 = Or(Xor(b1083,False),Xor(b1090,False)) | |
| b1092 = Or(Xor(b684,True),Xor(b691,True)) | |
| b1093 = Or(Xor(b698,True),Xor(b705,False)) | |
| b1094 = Or(Xor(b1092,False),Xor(b1093,False)) | |
| b1095 = Or(Xor(b712,True),Xor(b719,True)) | |
| b1096 = Or(Xor(b726,True),Xor(b733,True)) | |
| b1097 = Or(Xor(b1095,False),Xor(b1096,False)) | |
| b1098 = Or(Xor(b1094,False),Xor(b1097,False)) | |
| b1099 = Or(Xor(b740,True),Xor(b747,True)) | |
| b1100 = Or(Xor(b754,False),Xor(b761,True)) | |
| b1101 = Or(Xor(b1099,False),Xor(b1100,False)) | |
| b1102 = Or(Xor(b768,True),Xor(b775,True)) | |
| b1103 = Or(Xor(b782,True),Xor(b789,False)) | |
| b1104 = Or(Xor(b1102,False),Xor(b1103,False)) | |
| b1105 = Or(Xor(b1101,False),Xor(b1104,False)) | |
| b1106 = Or(Xor(b1098,False),Xor(b1105,False)) | |
| b1107 = Or(Xor(b1091,False),Xor(b1106,False)) | |
| b1108 = Or(Xor(b796,True),Xor(b803,True)) | |
| b1109 = Or(Xor(b810,False),Xor(b817,False)) | |
| b1110 = Or(Xor(b1108,False),Xor(b1109,False)) | |
| b1111 = Or(Xor(b824,False),Xor(b831,False)) | |
| b1112 = Or(Xor(b838,True),Xor(b845,False)) | |
| b1113 = Or(Xor(b1111,False),Xor(b1112,False)) | |
| b1114 = Or(Xor(b1110,False),Xor(b1113,False)) | |
| b1115 = Or(Xor(b852,True),Xor(b859,True)) | |
| b1116 = Or(Xor(b866,False),Xor(b873,True)) | |
| b1117 = Or(Xor(b1115,False),Xor(b1116,False)) | |
| b1118 = Or(Xor(b880,False),Xor(b887,False)) | |
| b1119 = Or(Xor(b894,False),Xor(b901,True)) | |
| b1120 = Or(Xor(b1118,False),Xor(b1119,False)) | |
| b1121 = Or(Xor(b1117,False),Xor(b1120,False)) | |
| b1122 = Or(Xor(b1114,False),Xor(b1121,False)) | |
| b1123 = Or(Xor(b908,False),Xor(b915,True)) | |
| b1124 = Or(Xor(b922,True),Xor(b929,False)) | |
| b1125 = Or(Xor(b1123,False),Xor(b1124,False)) | |
| b1126 = Or(Xor(b936,False),Xor(b943,True)) | |
| b1127 = Or(Xor(b950,False),Xor(b957,False)) | |
| b1128 = Or(Xor(b1126,False),Xor(b1127,False)) | |
| b1129 = Or(Xor(b1125,False),Xor(b1128,False)) | |
| b1130 = Or(Xor(b964,True),Xor(b971,False)) | |
| b1131 = Or(Xor(b978,False),Xor(b985,False)) | |
| b1132 = Or(Xor(b1130,False),Xor(b1131,False)) | |
| b1133 = Or(Xor(b992,False),Xor(b999,True)) | |
| b1134 = Or(Xor(b1006,True),Xor(b1013,True)) | |
| b1135 = Or(Xor(b1133,False),Xor(b1134,False)) | |
| b1136 = Or(Xor(b1132,False),Xor(b1135,False)) | |
| b1137 = Or(Xor(b1129,False),Xor(b1136,False)) | |
| b1138 = Or(Xor(b1122,False),Xor(b1137,False)) | |
| b1139 = Or(Xor(b1107,False),Xor(b1138,False)) | |
| b1140 = Or(Xor(b1076,False),Xor(b1139,False)) | |
| s = Solver() | |
| s.add(Xor(b1140,True) == True) | |
| r = s.check() | |
| if r == sat: | |
| print(s.model()) | |
| else: | |
| print('failed') |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment