-
-
Save Charo-IT/671dcda5b6de9c1483783e1aaedf5deb to your computer and use it in GitHub Desktop.
SECCON 2017 Quals - printf machine
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
| #coding:ascii-8bit | |
| def get_next_token(s) | |
| case s | |
| when /^%2\$\*(\d+)\$s(.*?)$/ | |
| token, s = [$1, $2] | |
| return [{op: :read, index: $1.to_i - 1 - 32}, s] | |
| when /^%(\d+)\$hhn(.*?)$/ | |
| token, s = [$1, $2] | |
| return [{op: :write, index: $1.to_i - 1}, s] | |
| when /^%2\$(\d+)s(.*?)$/ | |
| token, s = [$1, $2] | |
| return [{op: :read_imm, value: $1.to_i}, s] | |
| when /^%1\$s(.*?)$/ | |
| return [{op: :strlen}, $1] | |
| else | |
| raise s | |
| end | |
| end | |
| program = open("default.fs", "rb").read.lines.map(&:strip) | |
| outbuf = <<EOS | |
| from z3 import * | |
| s = Solver() | |
| b = [BitVec("b_%d" % i, 8) for i in range(32)] | |
| for i in range(16): | |
| s.add(b[i] == 0) | |
| EOS | |
| program.each{|l| | |
| a = [0] | |
| print "0" | |
| while l.length > 0 | |
| token, l = get_next_token(l) | |
| if token[:op] == :read | |
| print " + b[#{token[:index]}]" | |
| a << "b[#{token[:index]}]" | |
| elsif token[:op] == :write | |
| print " => b[#{token[:index]}];" | |
| outbuf << "b[#{token[:index]}] = #{a.join(" + ")}\n" | |
| elsif token[:op] == :read_imm | |
| print " + #{token[:value]}" | |
| a << token[:value] | |
| elsif token[:op] == :strlen | |
| print " + strlen(b)" | |
| outbuf << "s.add(b[0] == 0)\n" | |
| end | |
| end | |
| puts | |
| } | |
| puts | |
| outbuf << <<EOS | |
| r = s.check() | |
| if r == sat: | |
| m = s.model() | |
| else: | |
| print "unsat" | |
| exit(0) | |
| print m | |
| EOS | |
| open("solver.py", "wb"){|f| f.write(outbuf)} |
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
| from z3 import * | |
| s = Solver() | |
| b = [BitVec("b_%d" % i, 8) for i in range(32)] | |
| for i in range(16): | |
| s.add(b[i] == 0) | |
| b[3] = 0 + b[16] | |
| b[16] = 0 + b[29] | |
| b[29] = 0 + b[3] | |
| b[3] = 0 + b[17] | |
| b[17] = 0 + b[23] | |
| b[23] = 0 + b[3] | |
| b[3] = 0 + b[18] | |
| b[18] = 0 + b[26] | |
| b[26] = 0 + b[3] | |
| b[3] = 0 + b[21] | |
| b[21] = 0 + b[26] | |
| b[26] = 0 + b[3] | |
| b[3] = 0 + b[22] | |
| b[22] = 0 + b[30] | |
| b[30] = 0 + b[3] | |
| b[3] = 0 + b[23] | |
| b[23] = 0 + b[31] | |
| b[31] = 0 + b[3] | |
| b[3] = 0 + b[25] | |
| b[25] = 0 + b[30] | |
| b[30] = 0 + b[3] | |
| b[3] = 0 + b[26] | |
| b[26] = 0 + b[31] | |
| b[31] = 0 + b[3] | |
| b[3] = 0 + b[28] | |
| b[28] = 0 + b[30] | |
| b[30] = 0 + b[3] | |
| b[3] = 0 + b[29] | |
| b[29] = 0 + b[31] | |
| b[31] = 0 + b[3] | |
| b[3] = 0 + b[30] | |
| b[30] = 0 + b[31] | |
| b[31] = 0 + b[3] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 110 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 115 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 95 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 144 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 92 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 206 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 205 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 111 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 233 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 166 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 41 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 60 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 20 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 223 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 247 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| b[2] = 0 | |
| b[3] = 0 | |
| b[8] = 0 + b[16] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[17] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[18] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[19] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[20] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[21] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[22] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[23] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[24] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[25] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[26] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[27] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[28] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[29] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[30] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[3] = 0 | |
| b[8] = 0 + b[31] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[3] = 0 + b[3] + b[8] | |
| b[8] = 0 + b[8] + b[8] | |
| b[2] = 0 + b[2] + b[3] | |
| b[0] = 0 + b[2] + 80 | |
| s.add(b[0] == 0) | |
| b[4] = 0 | |
| b[15] = 0 + b[15] + b[4] | |
| r = s.check() | |
| if r == sat: | |
| m = s.model() | |
| else: | |
| print "unsat" | |
| exit(0) | |
| print m |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment