1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
| from z3 import * arr1 = [16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 18, 19, 17, 17, 17, 17, 16, 15, 18, 20, 20, 18, 16, 19, 19, 18, 20, 20, 19, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 18, 17, 17, 17, 17, 17, 17, 18, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 15, 15, 16, 15, 14, 13, 11, 11, 13, 13, 15, 17, 18, 12, 12, 14, 12, 16, 17, 14, 14, 18, 17, 16, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 18, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 14, 14, 13, 9, 10, 11, 10, 11, 17, 9, 11, 13, 15, 10, 9, 9, 10, 13, 15, 13, 17, 17, 19, 16, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 18, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 14, 14, 13, 14, 13, 15, 20, 16, 14, 14, 18, 16, 9, 14, 14, 11, 11, 7, 7, 10, 12, 15, 18, 20, 19, 18, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 18, 16, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 17, 15, 13, 13, 13, 16, 14, 17, 18, 16, 14, 17, 14, 17, 12, 10, 14, 14, 10, 11, 7, 8, 12, 17, 21, 20, 21, 21, 17, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 16, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 18, 17, 13, 12, 9, 9, 8, 7, 13, 17, 18, 15, 14, 15, 17, 15, 10, 13, 12, 9, 10, 9, 12, 14, 17, 20, 20, 21, 20, 17, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 16, 15, 15, 15, 15, 15, 15, 15, 15, 16, 19, 19, 17, 12, 11, 10, 11, 7, 7, 7, 9, 14, 15, 11, 9, 14, 17, 13, 10, 13, 12, 12, 15, 17, 15, 16, 17, 18, 18, 18, 18, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 16, 15, 15, 15, 15, 15, 15, 15, 15, 16, 19, 16, 16, 11, 7, 15, 13, 11, 9, 7, 7, 8, 8, 8, 9, 10, 13, 17, 15, 15, 13, 16, 19, 17, 14, 15, 15, 16, 14, 16, 17, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 16, 15, 15, 15, 15, 15, 15, 15, 15, 17, 19, 16, 14, 9, 8, 7, 6, 11, 11, 10, 6, 4, 1, 2, 2, 2, 7, 14, 17, 16, 15, 16, 19, 17, 9, 5, 9, 13, 13, 18, 20, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 14, 11, 11, 9, 7, 8, 8, 7, 9, 11, 6, 2, 5, 8, 9, 6, 1, 8, 14, 17, 15, 14, 18, 8, 8, 10, 5, 11, 14, 17, 20, 17, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 15, 15, 15, 15, 15, 15, 15, 15, 15, 14, 16, 12, 13, 8, 10, 9, 8, 9, 11, 9, 6, 6, 0, 3, 8, 5, 6, 4, 12, 17, 18, 17, 15, 7, 8, 7, 15, 14, 16, 18, 18, 18, 17, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 16, 16, 17, 17, 17, 15, 15, 15, 15, 15, 15, 15, 16, 16, 12, 14, 14, 13, 10, 9, 10, 10, 11, 11, 10, 4, 6, 0, 0, 0, 0, 9, 4, 10, 16, 19, 18, 12, 4, 0, 0, 9, 15, 17, 17, 18, 18, 17, 16, 16, 16, 16, 16, 16, 16, 18, 21, 21, 23, 19, 17, 17, 17, 17, 17, 16, 17, 17, 17, 15, 15, 15, 15, 15, 15, 15, 16, 14, 15, 16, 11, 9, 10, 10, 10, 10, 10, 12, 12, 6, 7, 0, 0, 0, 2, 10, 4, 12, 16, 16, 18, 17, 7, 0, 0, 10, 16, 18, 18, 21, 20, 18, 16, 16, 16, 16, 16, 16, 21, 20, 17, 16, 18, 19, 21, 17, 16, 16, 16, 16, 17, 16, 17, 15, 15, 15, 15, 15, 15, 15, 14, 16, 17, 15, 13, 11, 11, 11, 8, 9, 12, 14, 14, 12, 6, 7, 2, 4, 11, 6, 5, 13, 15, 17, 18, 18, 14, 6, 7, 13, 18, 17, 14, 16, 20, 16, 16, 16, 15, 16, 16, 18, 20, 16, 16, 16, 16, 16, 21, 16, 16, 16, 16, 16, 16, 16, 17, 15, 15, 15, 15, 15, 15, 15, 13, 15, 14, 13, 11, 10, 10, 10, 11, 9, 11, 13, 13, 15, 12, 6, 10, 10, 5, 9, 10, 13, 14, 12, 19, 17, 14, 12, 11, 14, 21, 18, 17, 18, 19, 18, 16, 15, 15, 16, 16, 20, 17, 16, 16, 16, 16, 16, 21, 16, 16, 16, 16, 16, 16, 16, 17, 15, 15, 15, 15, 15, 15, 16, 13, 12, 11, 10, 9, 10, 9, 10, 8, 7, 8, 11, 13, 15, 16, 14, 11, 11, 12, 10, 10, 12, 12, 10, 18, 16, 19, 16, 16, 17, 20, 17, 16, 14, 18, 18, 16, 15, 15, 15, 16, 22, 16, 16, 16, 16, 16, 16, 21, 16, 16, 16, 16, 16, 16, 16, 17, 15, 15, 15, 15, 15, 15, 16, 14, 10, 8, 8, 8, 8, 7, 10, 8, 5, 6, 7, 12, 16, 15, 15, 13, 11, 10, 5, 6, 10, 11, 7, 15, 15, 14, 11, 17, 17, 17, 17, 16, 16, 15, 16, 15, 15, 15, 15, 16, 21, 16, 16, 16, 16, 16, 16, 21, 16, 16, 16, 16, 16, 16, 16, 17, 15, 15, 15, 15, 15, 15, 15, 14, 9, 7, 7, 10, 9, 6, 10, 12, 6, 3, 7, 10, 13, 16, 10, 6, 6, 8, 6, 3, 2, 5, 3, 9, 15, 11, 7, 8, 13, 18, 14, 15, 16, 16, 16, 15, 15, 15, 15, 16, 21, 16, 16, 16, 16, 16, 17, 21, 16, 16, 16, 16, 16, 16, 16, 17, 15, 15, 15, 15, 15, 15, 16, 13, 9, 10, 11, 10, 8, 4, 8, 12, 9, 7, 6, 6, 12, 13, 7, 7, 7, 9, 9, 6, 4, 1, 1, 4, 13, 12, 9, 5, 5, 10, 13, 13, 16, 18, 16, 15, 15, 15, 15, 15, 17, 22, 20, 19, 19, 20, 22, 17, 16, 16, 16, 16, 16, 16, 16, 17, 15, 15, 15, 15, 15, 15, 16, 12, 10, 15, 13, 10, 10, 6, 3, 7, 12, 9, 5, 5, 11, 11, 9, 11, 13, 13, 10, 7, 5, 1, 1, 2, 14, 18, 17, 9, 6, 8, 10, 14, 15, 18, 16, 15, 15, 15, 15, 15, 15, 16, 17, 18, 18, 18, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 12, 13, 13, 15, 10, 11, 9, 4, 7, 11, 10, 9, 5, 10, 11, 14, 13, 14, 13, 10, 9, 8, 7, 5, 3, 9, 15, 19, 20, 13, 9, 9, 10, 13, 19, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 17, 17, 11, 14, 10, 10, 7, 6, 3, 6, 10, 12, 6, 7, 14, 13, 14, 12, 16, 14, 12, 8, 6, 5, 4, 6, 9, 17, 20, 20, 11, 6, 9, 12, 21, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 19, 17, 9, 11, 8, 6, 8, 9, 5, 5, 6, 8, 9, 11, 10, 13, 11, 12, 13, 17, 15, 9, 6, 3, 4, 6, 16, 18, 19, 20, 15, 7, 8, 13, 19, 17, 16, 16, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 18, 13, 11, 9, 7, 6, 9, 10, 10, 11, 14, 9, 9, 14, 10, 12, 8, 8, 13, 12, 15, 11, 6, 9, 7, 8, 17, 21, 21, 21, 16, 12, 15, 15, 18, 19, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 15, 14, 14, 14, 9, 6, 7, 10, 14, 12, 9, 11, 11, 13, 12, 8, 6, 7, 8, 12, 10, 9, 11, 14, 12, 8, 6, 10, 11, 11, 17, 19, 14, 14, 16, 18, 18, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 15, 15, 15, 15, 15, 15, 14, 17, 14, 15, 11, 7, 6, 11, 10, 7, 4, 7, 10, 14, 14, 12, 8, 6, 3, 4, 3, 2, 6, 8, 5, 5, 2, 6, 6, 7, 13, 17, 14, 10, 13, 15, 15, 17, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 15, 14, 14, 14, 15, 15, 15, 16, 11, 14, 13, 10, 8, 5, 7, 5, 3, 4, 8, 14, 16, 9, 5, 7, 8, 8, 5, 2, 6, 8, 6, 5, 7, 10, 5, 5, 12, 12, 8, 8, 8, 13, 16, 17, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 15, 14, 14, 14, 14, 14, 15, 10, 8, 12, 11, 16, 7, 5, 3, 4, 2, 2, 5, 9, 13, 10, 3, 4, 10, 13, 10, 5, 6, 9, 6, 5, 12, 8, 5, 6, 12, 9, 6, 6, 5, 10, 15, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 15, 14, 14, 14, 14, 14, 12, 8, 6, 8, 13, 15, 4, 4, 3, 2, 0, 1, 2, 4, 8, 8, 2, 3, 7, 13, 11, 10, 7, 9, 5, 9, 11, 6, 4, 10, 10, 8, 4, 7, 4, 9, 13, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 16, 14, 14, 14, 14, 15, 12, 9, 6, 5, 7, 13, 12, 2, 2, 4, 1, 0, 0, 1, 4, 8, 7, 2, 3, 5, 7, 12, 15, 10, 9, 6, 10, 8, 3, 3, 12, 8, 4, 5, 8, 4, 7, 13, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 16, 16, 14, 14, 14, 14, 13, 10, 6, 5, 6, 7, 15, 8, 1, 2, 4, 2, 2, 1, 1, 4, 5, 5, 5, 8, 5, 5, 12, 16, 11, 12, 11, 10, 7, 5, 5, 11, 5, 5, 5, 9, 8, 11, 11, 15, 15, 14, 15, 16, 21, 16, 15, 15, 15, 15, 15, 15, 15, 20, 15, 15, 15, 15, 15, 16, 14, 14, 14, 15, 11, 8, 5, 6, 6, 9, 15, 4, 2, 5, 4, 1, 5, 3, 1, 5, 4, 4, 7, 8, 6, 7, 11, 16, 13, 15, 12, 9, 7, 8, 11, 8, 7, 7, 5, 9, 12, 12, 10, 18, 15, 14, 15, 21, 15, 15, 15, 15, 15, 15, 15, 15, 15, 21, 15, 15, 15, 15, 15, 16, 14, 14, 14, 13, 8, 7, 5, 5, 8, 14, 11, 5, 11, 9, 2, 4, 7, 3, 2, 4, 2, 3, 6, 8, 7, 8, 11, 12, 16, 16, 13, 11, 8, 9, 12, 10, 7, 12, 4, 9, 16, 10, 8, 18, 15, 14, 18, 18, 15, 15, 15, 15, 15, 15, 15, 15, 15, 21, 16, 15, 15, 15, 15, 16, 14, 14, 14, 9, 7, 5, 4, 7, 15, 15, 8, 12, 13, 3, 2, 5, 7, 2, 4, 6, 2, 2, 5, 9, 11, 11, 12, 13, 14, 17, 16, 12, 11, 12, 13, 10, 9, 15, 3, 7, 16, 13, 8, 17, 16, 15, 22, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 21, 16, 15, 15, 15, 15, 16, 14, 14, 11, 9, 4, 3, 9, 14, 11, 8, 6, 14, 8, 2, 2, 6, 4, 2, 6, 7, 3, 4, 4, 9, 13, 13, 13, 12, 12, 16, 17, 11, 13, 14, 12, 11, 9, 15, 3, 4, 12, 17, 9, 15, 17, 17, 19, 14, 15, 15, 15, 19, 15, 15, 15, 15, 15, 21, 16, 15, 15, 15, 15, 16, 14, 14, 10, 11, 4, 2, 12, 7, 14, 4, 6, 14, 12, 4, 1, 4, 3, 4, 5, 7, 5, 6, 3, 6, 12, 12, 11, 10, 12, 12, 17, 11, 14, 16, 8, 9, 10, 17, 7, 5, 7, 17, 10, 16, 18, 18, 18, 14, 14, 15, 15, 24, 17, 15, 15, 15, 15, 21, 15, 15, 15, 15, 15, 16, 14, 13, 12, 7, 5, 5, 7, 10, 14, 5, 5, 10, 14, 3, 1, 4, 6, 4, 2, 8, 8, 7, 2, 5, 8, 10, 10, 9, 12, 10, 16, 11, 13, 13, 6, 7, 10, 17, 14, 7, 5, 13, 9, 16, 18, 15, 22, 18, 16, 17, 19, 21, 20, 15, 15, 15, 15, 22, 15, 15, 15, 15, 15, 16, 14, 13, 15, 5, 1, 7, 5, 10, 7, 6, 6, 13, 10, 1, 1, 6, 8, 3, 2, 8, 9, 8, 3, 3, 7, 9, 8, 8, 10, 9, 12, 12, 10, 10, 5, 5, 8, 15, 18, 5, 8, 11, 11, 17, 16, 14, 15, 18, 19, 19, 18, 15, 20, 21, 19, 20, 22, 18, 15, 15, 15, 15, 15, 16, 14, 13, 12, 4, 9, 2, 5, 9, 9, 6, 8, 10, 8, 2, 5, 7, 6, 1, 2, 6, 7, 9, 5, 1, 5, 9, 5, 4, 8, 9, 15, 10, 7, 5, 3, 4, 6, 13, 16, 9, 11, 15, 15, 19, 16, 14, 14, 14, 14, 14, 15, 15, 15, 16, 17, 17, 15, 15, 15, 15, 15, 15, 15, 15, 14, 13, 10, 5, 9, 3, 5, 8, 13, 9, 11, 11, 10, 6, 5, 6, 4, 2, 3, 4, 4, 10, 8, 1, 3, 10, 7, 3, 8, 10, 10, 10, 3, 3, 4, 3, 7, 11, 13, 10, 14, 15, 19, 18, 16, 14, 14, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 16, 13, 13, 14, 12, 12, 5, 6, 13, 14, 11, 11, 10, 8, 4, 5, 4, 3, 2, 6, 3, 1, 8, 11, 3, 2, 7, 9, 6, 8, 12, 8, 9, 2, 5, 5, 3, 9, 9, 11, 12, 16, 15, 18, 16, 14, 14, 14, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 13, 13, 16, 17, 11, 7, 10, 15, 13, 11, 8, 7, 9, 6, 4, 6, 3, 2, 7, 7, 1, 4, 11, 6, 1, 3, 8, 8, 8, 10, 8, 3, 2, 4, 7, 6, 10, 5, 10, 16, 21, 20, 17, 14, 14, 14, 14, 14, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 13, 13, 17, 18, 16, 11, 18, 18, 16, 13, 9, 7, 7, 2, 5, 7, 4, 2, 5, 10, 7, 1, 10, 9, 2, 1, 5, 8, 8, 10, 7, 2, 2, 4, 9, 6, 9, 6, 9, 18, 23, 21, 14, 13, 13, 14, 14, 14, 14, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 13, 13, 17, 18, 16, 14, 22, 19, 16, 10, 8, 8, 4, 2, 5, 7, 7, 4, 3, 9, 13, 10, 6, 11, 5, 0, 3, 8, 10, 10, 4, 1, 1, 6, 5, 6, 9, 11, 10, 17, 22, 17, 13, 13, 13, 13, 14, 14, 14, 14, 20, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 13, 13, 18, 19, 17, 14, 19, 12, 12, 10, 10, 6, 4, 4, 7, 8, 8, 5, 2, 8, 11, 11, 9, 12, 9, 3, 3, 8, 10, 6, 3, 1, 3, 5, 2, 8, 11, 10, 13, 14, 18, 15, 13, 13, 13, 13, 13, 14, 14, 14, 20, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 13, 13, 16, 19, 18, 16, 17, 9, 11, 11, 9, 6, 7, 7, 8, 8, 6, 5, 1, 5, 10, 10, 8, 6, 7, 5, 4, 8, 7, 2, 3, 3, 3, 3, 4, 7, 10, 10, 13, 13, 14, 13, 13, 13, 13, 13, 13, 13, 14, 17, 18, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15, 15, 13, 13, 15, 20, 19, 15, 18, 11, 12, 10, 9, 4, 7, 6, 7, 7, 6, 4, 2, 3, 7, 10, 10, 7, 7, 4, 7, 7, 3, 3, 3, 3, 3, 5, 6, 9, 9, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 14, 14, 19, 15, 14, 14, 14, 14, 15, 14, 15, 15, 15, 15, 15, 15, 15, 13, 13, 13, 19, 20, 14, 17, 14, 13, 11, 10, 4, 7, 4, 6, 6, 7, 5, 3, 4, 5, 8, 10, 10, 5, 1, 5, 2, 1, 3, 4, 2, 4, 7, 9, 8, 13, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 14, 13, 21, 14, 14, 14, 14, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 13, 13, 13, 14, 15, 13, 17, 17, 13, 13, 10, 3, 6, 5, 7, 6, 5, 4, 4, 3, 5, 5, 7, 10, 9, 5, 4, 3, 4, 3, 1, 3, 8, 13, 9, 8, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 15, 21, 14, 14, 14, 14, 14, 14, 14, 15, 15, 15, 14, 14, 14, 15, 13, 13, 13, 13, 13, 13, 14, 18, 12, 8, 9, 3, 6, 6, 8, 8, 5, 2, 3, 2, 2, 6, 8, 7, 6, 6, 5, 3, 1, 2, 3, 8, 13, 11, 7, 16, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 17, 18, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 15, 13, 13, 13, 13, 13, 13, 13, 16, 11, 5, 7, 5, 6, 6, 7, 7, 8, 3, 1, 4, 4, 4, 6, 9, 8, 6, 6, 4, 1, 3, 8, 10, 7, 8, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 19, 16, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 15, 18, 13, 13, 12, 13, 13, 13, 13, 13, 12, 8, 7, 9, 6, 3, 4, 6, 8, 7, 2, 2, 7, 7, 7, 7, 7, 6, 5, 3, 0, 4, 6, 3, 6, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 21, 14, 14, 14, 16, 14, 14, 14, 14, 14, 14, 14, 14, 15, 19, 20, 13, 12, 13, 13, 13, 13, 13, 13, 12, 11, 10, 9, 10, 5, 1, 2, 3, 7, 5, 2, 3, 6, 6, 6, 6, 5, 3, 1, 2, 3, 3, 5, 9, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 21, 14, 14, 14, 21, 14, 14, 14, 16, 18, 20, 18, 15, 18, 21, 21, 13, 13, 13, 13, 13, 13, 13, 13, 13, 12, 14, 14, 12, 10, 2, 3, 2, 2, 3, 4, 4, 4, 5, 5, 4, 3, 2, 2, 1, 1, 2, 6, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 14, 21, 14, 14, 16, 20, 16, 22, 23, 22, 23, 23, 24, 23, 20, 24, 22, 13, 12, 13, 12, 13, 13, 13, 13, 13, 13, 14, 14, 14, 11, 9, 8, 5, 4, 2, 4, 5, 7, 8, 9, 8, 8, 5, 3, 2, 2, 6, 4, 11, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 20, 15, 13, 21, 15, 14, 19, 22, 23, 23, 24, 24, 24, 24, 24, 21, 13, 12, 12, 13, 13, 12, 13, 13, 13, 13, 13, 15, 15, 14, 9, 7, 6, 2, 3, 7, 9, 10, 11, 11, 10, 10, 8, 4, 3, 2, 4, 5, 12, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 15, 20, 17, 19, 13, 15, 20, 21, 22, 22, 22, 19, 23, 24, 24, 24, 13, 13, 12, 13, 13, 12, 13, 13, 13, 13, 13, 13, 13, 13, 10, 6, 3, 2, 7, 8, 10, 11, 12, 12, 12, 13, 13, 5, 3, 2, 3, 8, 12, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 17, 20, 14, 13, 14, 18, 19, 20, 20, 21, 20, 20, 21, 22, 20, 13, 13, 12, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 10, 6, 6, 6, 10, 11, 11, 12, 13, 14, 15, 16, 16, 8, 6, 4, 5, 9, 11, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 15, 14, 13, 14, 15, 14, 15, 15, 17, 18, 19, 19, 19, 19, 19, 20, 20, 19, 13, 12, 13, 13, 13, 12, 12, 13, 13, 13, 13, 13, 13, 14, 12, 9, 8, 10, 10, 12, 14, 14, 16, 18, 19, 19, 18, 13, 10, 10, 7, 9, 15, 19, 17, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 14, 14, 18, 17, 19, 19, 19, 19, 15, 16, 14, 13, 19, 18, 18, 18, 13, 16, 17, 13, 12, 13, 13, 13, 12, 13, 13, 13, 13, 13, 13, 13, 13, 18, 16, 12, 11, 16, 16, 17, 18, 20, 20, 22, 20, 18, 16, 13, 13, 12, 8, 9, 14, 19, 18, 17, 19, 18, 14, 13, 14, 15, 14, 14, 18, 17, 17, 17, 17, 17, 17, 16, 16, 13, 13, 13, 12, 14, 15, 16, 17, 17, 18, 12, 12, 12, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 21, 18, 13, 11, 17, 19, 20, 21, 20, 18, 19, 18, 14, 14, 13, 13, 13, 9, 7, 12, 18, 18, 16, 16, 19, 20, 17, 16, 16, 18, 17, 15, 14, 13, 12, 13, 14, 13, 12, 10, 10, 9, 12, 16, 16, 18, 19, 18, 18, 19, 12, 12, 12, 12, 13, 12, 12, 13, 13, 13, 13, 13, 13, 17, 21, 20, 16, 13, 14, 14, 16, 16, 16, 16, 14, 15, 13, 13, 13, 13, 13, 12, 7, 10, 14, 20, 13, 14, 16, 20, 20, 17, 16, 12, 14, 11, 14, 15, 10, 11, 13, 10, 8, 9, 9, 8, 14, 19, 19, 18, 18, 18, 18, 19, 12, 12, 12, 13, 12, 13, 13, 13, 13, 13, 13, 13, 15, 22, 22, 20, 15, 13, 13, 10, 9, 9, 10, 11, 11, 9, 10, 13, 12, 11, 10, 10, 9, 10, 9, 19, 17, 8, 8, 15, 21, 16, 11, 10, 10, 12, 10, 9, 8, 11, 8, 8, 6, 9, 13, 9, 9, 12, 16, 18, 17, 16, 18, 20, 13, 13, 13, 13, 13, 13, 13, 13, 13, 14, 15, 20, 22, 22, 22, 22, 16, 12, 8, 8, 6, 6, 8, 7, 7, 6, 7, 10, 8, 9, 8, 11, 9, 8, 6, 12, 16, 10, 6, 11, 15, 14, 10, 12, 11, 11, 11, 9, 7, 9, 8, 11, 10, 8, 7, 8, 9, 18, 20, 20, 19, 19, 17, 19] arr2 = [15, 14, 14, 13, 13, 14, 14, 13, 12, 10, 13, 21, 17, 14, 11, 10, 11, 16, 17, 8, 8, 7, 10, 12, 13, 12, 16, 18, 9, 6, 7, 8, 7, 8, 9, 8, 9, 10, 12, 12, 14, 16, 16, 14, 9, 4, 3, 5, 6, 6, 6, 3, 4, 6, 6, 5, 5, 5, 5, 4, 5, 7, 5, 4, 15, 15, 14, 13, 13, 14, 14, 13, 12, 11, 21, 15, 15, 14, 11, 10, 8, 8, 10, 8, 8, 7, 9, 11, 11, 11, 19, 13, 12, 5, 6, 7, 7, 8, 9, 9, 10, 12, 15, 17, 17, 17, 16, 10, 4, 4, 5, 6, 7, 7, 6, 4, 5, 7, 6, 6, 5, 5, 4, 3, 5, 6, 4, 3, 15, 15, 14, 13, 13, 14, 14, 13, 12, 19, 15, 13, 15, 14, 12, 10, 8, 8, 9, 8, 8, 7, 9, 10, 9, 16, 14, 8, 17, 5, 6, 9, 16, 17, 17, 18, 18, 19, 21, 22, 22, 21, 19, 10, 4, 5, 6, 7, 9, 9, 6, 5, 8, 8, 6, 6, 5, 4, 4, 3, 3, 4, 3, 3, 15, 15, 14, 14, 13, 14, 14, 14, 14, 19, 12, 13, 14, 14, 13, 12, 10, 9, 9, 9, 8, 7, 9, 10, 12, 18, 10, 8, 18, 6, 6, 7, 7, 6, 7, 8, 9, 12, 15, 20, 14, 10, 5, 4, 5, 6, 7, 9, 10, 10, 7, 7, 9, 9, 7, 6, 6, 5, 6, 6, 6, 6, 5, 5, 15, 14, 14, 13, 13, 14, 14, 14, 15, 18, 11, 12, 13, 14, 14, 14, 12, 11, 11, 11, 10, 10, 11, 14, 23, 18, 18, 18, 20, 12, 7, 7, 7, 6, 6, 8, 10, 13, 14, 20, 11, 6, 4, 5, 6, 7, 9, 10, 11, 10, 7, 9, 11, 9, 7, 6, 6, 6, 7, 7, 7, 7, 7, 6, 15, 15, 14, 14, 13, 14, 15, 14, 12, 20, 8, 8, 11, 14, 14, 14, 13, 17, 22, 15, 12, 12, 14, 22, 14, 13, 12, 9, 8, 19, 7, 7, 7, 6, 6, 7, 9, 12, 13, 20, 10, 7, 6, 6, 8, 9, 10, 12, 12, 10, 9, 11, 11, 10, 8, 7, 7, 7, 7, 8, 7, 7, 7, 6, 15, 14, 14, 14, 13, 14, 15, 13, 7, 10, 16, 4, 5, 12, 15, 19, 22, 19, 13, 12, 12, 13, 22, 15, 13, 13, 12, 9, 7, 17, 11, 8, 7, 6, 5, 6, 9, 12, 13, 20, 11, 10, 8, 8, 9, 11, 11, 13, 12, 10, 11, 12, 11, 11, 9, 8, 7, 7, 8, 8, 8, 7, 7, 6, 14, 14, 14, 14, 13, 13, 14, 11, 3, 2, 9, 17, 18, 19, 19, 18, 13, 12, 12, 12, 12, 16, 18, 13, 13, 13, 11, 9, 8, 14, 13, 7, 8, 6, 5, 6, 9, 11, 12, 20, 12, 11, 10, 10, 11, 12, 12, 13, 12, 11, 12, 13, 12, 11, 10, 8, 8, 8, 8, 8, 8, 7, 7, 6, 14, 14, 14, 14, 13, 13, 14, 7, 2, 4, 4, 4, 4, 3, 3, 9, 10, 10, 11, 11, 12, 12, 12, 12, 12, 12, 11, 8, 7, 5, 4, 6, 7, 6, 5, 5, 8, 10, 11, 20, 13, 12, 11, 11, 12, 13, 13, 13, 13, 12, 13, 13, 13, 12, 10, 9, 8, 8, 8, 8, 8, 7, 7, 6, 15, 14, 14, 14, 13, 13, 13, 3, 4, 5, 5, 5, 4, 3, 3, 3, 7, 9, 11, 12, 13, 12, 13, 12, 12, 11, 9, 7, 5, 5, 5, 5, 4, 3, 3, 3, 3, 4, 7, 11, 11, 12, 12, 12, 13, 13, 14, 13, 13, 13, 13, 14, 13, 12, 11, 9, 8, 8, 8, 8, 8, 7, 6, 5, 15, 15, 14, 14, 13, 13, 11, 3, 5, 6, 6, 4, 4, 3, 3, 3, 3, 9, 13, 13, 13, 12, 10, 11, 9, 8, 7, 5, 4, 3, 3, 2, 2, 1, 1, 1, 1, 2, 2, 4, 7, 10, 11, 13, 14, 13, 14, 14, 13, 14, 14, 13, 13, 12, 11, 10, 9, 8, 8, 8, 8, 7, 6, 5, 15, 15, 14, 14, 13, 13, 9, 3, 5, 6, 5, 5, 4, 4, 3, 2, 2, 4, 11, 12, 10, 8, 7, 5, 4, 4, 4, 3, 3, 2, 2, 2, 1, 1, 1, 1, 1, 2, 2, 3, 4, 4, 5, 9, 13, 13, 14, 13, 14, 13, 13, 13, 13, 12, 11, 9, 9, 8, 8, 8, 8, 7, 5, 6, 15, 14, 14, 14, 13, 13, 7, 4, 6, 6, 5, 4, 4, 3, 3, 2, 2, 2, 4, 9, 9, 5, 3, 2, 2, 2, 2, 3, 3, 3, 2, 2, 1, 1, 1, 1, 1, 2, 2, 5, 5, 3, 2, 2, 6, 12, 13, 13, 13, 14, 14, 13, 12, 11, 9, 8, 7, 7, 7, 7, 8, 7, 5, 6, 15, 14, 14, 14, 13, 12, 4, 5, 7, 6, 5, 4, 4, 3, 3, 2, 2, 2, 3, 4, 4, 2, 2, 2, 2, 2, 1, 2, 3, 3, 3, 3, 2, 1, 1, 1, 2, 2, 4, 6, 6, 3, 2, 2, 2, 5, 9, 12, 14, 14, 12, 8, 6, 5, 5, 6, 7, 6, 6, 6, 7, 6, 5, 6, 15, 14, 14, 14, 13, 11, 4, 5, 7, 6, 5, 5, 4, 4, 3, 3, 3, 2, 2, 2, 2, 4, 7, 9, 10, 9, 7, 4, 2, 4, 4, 4, 4, 3, 2, 2, 2, 2, 4, 4, 4, 4, 4, 3, 3, 4, 5, 9, 12, 10, 4, 3, 4, 3, 3, 4, 6, 6, 7, 8, 7, 5, 4, 6, 15, 14, 14, 14, 13, 10, 3, 5, 7, 6, 5, 4, 4, 3, 3, 3, 3, 3, 2, 2, 7, 13, 13, 12, 13, 18, 14, 10, 5, 1, 4, 4, 4, 5, 5, 4, 3, 2, 4, 4, 3, 4, 5, 6, 5, 6, 6, 5, 6, 5, 4, 4, 5, 4, 4, 3, 5, 7, 8, 9, 6, 3, 2, 3, 14, 14, 14, 14, 13, 9, 4, 6, 7, 7, 5, 5, 4, 3, 3, 3, 3, 3, 2, 8, 16, 17, 15, 10, 7, 9, 15, 13, 11, 5, 2, 3, 6, 6, 7, 4, 2, 2, 3, 1, 0, 1, 4, 3, 5, 4, 5, 6, 4, 3, 4, 4, 4, 5, 4, 3, 5, 9, 10, 10, 6, 3, 2, 2, 14, 14, 14, 13, 13, 7, 4, 5, 7, 7, 6, 5, 4, 4, 4, 4, 3, 3, 6, 16, 18, 17, 6, 4, 2, 3, 3, 13, 14, 9, 3, 3, 3, 5, 4, 2, 2, 1, 1, 0, 0, 0, 3, 2, 4, 1, 1, 3, 2, 2, 4, 5, 6, 5, 5, 4, 4, 9, 10, 8, 5, 2, 2, 3, 14, 14, 14, 13, 13, 6, 6, 5, 7, 7, 7, 6, 5, 4, 4, 4, 4, 5, 9, 17, 19, 16, 5, 3, 2, 2, 2, 10, 13, 11, 4, 3, 3, 1, 2, 2, 1, 0, 0, 0, 0, 1, 3, 1, 3, 0, 1, 3, 6, 7, 5, 4, 4, 5, 5, 5, 4, 11, 10, 7, 4, 3, 3, 5, 14, 14, 13, 13, 13, 6, 6, 6, 6, 6, 6, 6, 5, 4, 3, 3, 3, 4, 6, 8, 12, 11, 6, 2, 2, 2, 2, 2, 4, 3, 1, 1, 2, 3, 2, 3, 2, 1, 1, 1, 2, 2, 2, 1, 2, 1, 0, 3, 12, 16, 15, 10, 6, 4, 5, 5, 4, 12, 12, 10, 8, 6, 6, 8, 14, 13, 13, 13, 12, 6, 6, 7, 6, 6, 6, 5, 4, 3, 3, 3, 3, 3, 4, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 2, 2, 3, 3, 3, 2, 3, 2, 2, 2, 2, 3, 2, 2, 2, 2, 4, 1, 2, 6, 11, 17, 17, 11, 8, 5, 5, 4, 11, 13, 11, 11, 9, 8, 9, 14, 13, 13, 13, 12, 5, 4, 7, 6, 6, 5, 4, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 2, 2, 3, 3, 2, 3, 3, 3, 3, 2, 1, 1, 2, 3, 3, 2, 3, 3, 3, 4, 4, 4, 4, 11, 16, 14, 8, 5, 4, 10, 11, 11, 12, 11, 9, 8, 13, 13, 13, 13, 10, 2, 3, 5, 6, 6, 4, 3, 2, 2, 2, 1, 1, 1, 2, 1, 1, 1, 1, 2, 1, 1, 1, 2, 2, 3, 2, 3, 3, 3, 3, 2, 1, 1, 1, 1, 1, 3, 3, 2, 3, 2, 3, 4, 5, 5, 4, 2, 14, 17, 14, 5, 4, 9, 10, 10, 11, 11, 9, 9, 12, 12, 12, 12, 10, 4, 3, 3, 5, 5, 3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 3, 2, 2, 3, 5, 3, 2, 3, 2, 2, 2, 2, 2, 2, 3, 2, 2, 2, 1, 1, 2, 3, 5, 5, 5, 11, 19, 17, 6, 5, 11, 12, 11, 11, 11, 10, 10, 12, 12, 12, 12, 9, 5, 4, 2, 4, 4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 2, 2, 2, 4, 3, 2, 2, 3, 2, 2, 2, 2, 3, 2, 2, 3, 1, 1, 2, 3, 3, 2, 3, 4, 5, 6, 8, 17, 19, 7, 5, 12, 12, 12, 11, 11, 11, 11, 11, 11, 11, 11, 9, 3, 3, 4, 3, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3, 2, 2, 2, 1, 0, 1, 2, 3, 4, 3, 3, 3, 4, 5, 5, 7, 12, 6, 5, 11, 11, 11, 11, 11, 11, 11, 12, 12, 13, 12, 9, 2, 2, 3, 3, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 2, 2, 2, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 1, 2, 2, 1, 1, 1, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 3, 3, 5, 10, 11, 11, 11, 12, 12, 13, 13, 13, 14, 12, 3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 0, 1, 1, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 1, 1, 1, 1, 2, 2, 2, 2, 2, 4, 5, 8, 10, 11, 12, 8, 5, 3, 2, 2, 3, 2, 2, 3, 4, 4, 3, 2, 2, 2, 4, 11, 12, 12, 12, 13, 14, 14, 14, 14, 14, 13, 3, 2, 2, 1, 1, 1, 1, 2, 2, 2, 2, 1, 1, 0, 1, 1, 1, 2, 2, 2, 2, 1, 1, 1, 1, 1, 2, 2, 1, 3, 10, 13, 14, 14, 15, 15, 17, 16, 14, 12, 11, 8, 3, 2, 2, 2, 3, 3, 3, 2, 2, 2, 3, 10, 12, 12, 13, 13, 14, 14, 15, 15, 14, 13, 4, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 2, 2, 1, 1, 1, 1, 2, 2, 1, 1, 1, 1, 0, 1, 1, 1, 1, 2, 9, 12, 17, 18, 17, 16, 15, 17, 17, 16, 16, 15, 16, 15, 4, 2, 2, 2, 3, 3, 3, 2, 2, 3, 10, 13, 13, 13, 14, 15, 15, 15, 15, 15, 13, 4, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 1, 1, 1, 2, 1, 1, 1, 1, 0, 1, 1, 0, 1, 1, 1, 1, 1, 1, 2, 8, 12, 18, 19, 17, 15, 17, 18, 18, 18, 18, 17, 15, 4, 2, 2, 2, 2, 3, 2, 2, 2, 3, 10, 14, 14, 14, 14, 16, 15, 15, 15, 14, 11, 2, 1, 1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 2, 9, 12, 14, 16, 14, 17, 16, 16, 17, 15, 13, 10, 1, 2, 1, 2, 2, 2, 3, 2, 1, 3, 11, 13, 13, 14, 15, 16, 15, 15, 15, 14, 7, 2, 2, 1, 1, 1, 1, 1, 0, 0, 0, 1, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 3, 9, 11, 12, 13, 13, 12, 12, 12, 12, 10, 3, 2, 1, 1, 1, 1, 1, 2, 2, 2, 4, 13, 15, 14, 14, 15, 16, 15, 15, 15, 12, 4, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 0, 1, 2, 2, 6, 9, 11, 10, 11, 11, 10, 9, 4, 1, 2, 1, 1, 1, 1, 1, 2, 1, 2, 4, 12, 14, 15, 15, 16, 17, 16, 15, 16, 16, 3, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, 0, 2, 1, 0, 0, 0, 0, 0, 0, 1, 2, 1, 2, 1, 2, 4, 6, 6, 5, 3, 1, 0, 1, 2, 1, 1, 1, 1, 1, 2, 2, 1, 4, 13, 14, 13, 15, 16, 16, 18, 19, 19, 18, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 2, 0, 0, 0, 0, 0, 0, 1, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 5, 14, 15, 15, 15, 15, 19, 19, 19, 19, 19, 12, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 2, 1, 0, 0, 0, 0, 1, 1, 2, 2, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 6, 12, 16, 16, 16, 16, 19, 19, 19, 19, 19, 16, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 1, 1, 1, 1, 2, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 0, 1, 2, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 8, 17, 15, 16, 18, 18, 19, 20, 20, 20, 20, 16, 3, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 2, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 2, 12, 18, 20, 18, 17, 20, 19, 20, 20, 20, 19, 17, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 2, 12, 20, 20, 20, 20, 18, 19, 19, 20, 19, 19, 18, 10, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 2, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 2, 5, 16, 17, 20, 20, 21, 21, 18, 18, 18, 19, 19, 18, 12, 2, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 9, 18, 19, 18, 21, 20, 21, 13, 14, 15, 15, 17, 18, 15, 4, 1, 1, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1, 1, 2, 14, 20, 19, 20, 19, 21, 20, 9, 12, 12, 9, 11, 16, 14, 6, 1, 1, 1, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 3, 16, 21, 21, 19, 20, 18, 21, 10, 10, 10, 10, 12, 13, 13, 7, 1, 1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 10, 17, 20, 21, 20, 19, 20, 19, 11, 12, 14, 14, 16, 17, 13, 8, 2, 1, 1, 1, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 1, 0, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 15, 20, 19, 20, 21, 20, 20, 20, 17, 18, 17, 19, 20, 19, 18, 12, 2, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 6, 19, 20, 19, 20, 20, 21, 20, 21, 19, 18, 20, 20, 20, 20, 19, 13, 3, 1, 2, 1, 1, 1, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 15, 20, 21, 20, 19, 21, 21, 22, 20, 19, 19, 20, 20, 20, 19, 18, 14, 3, 2, 1, 1, 1, 1, 0, 1, 1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0, 1, 5, 20, 21, 21, 21, 19, 21, 22, 22, 21, 20, 20, 20, 20, 19, 19, 18, 13, 3, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 9, 21, 21, 21, 21, 21, 19, 22, 22, 22, 20, 20, 20, 20, 19, 19, 17, 9, 2, 1, 1, 1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 14, 22, 22, 22, 22, 21, 20, 22, 22, 22, 19, 20, 20, 20, 20, 18, 13, 4, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 5, 18, 22, 22, 22, 21, 21, 21, 20, 22, 22, 15, 16, 17, 17, 17, 14, 7, 2, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 12, 22, 24, 23, 22, 23, 23, 21, 20, 22, 22, 13, 12, 12, 11, 11, 8, 3, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 2, 21, 25, 25, 25, 25, 25, 25, 21, 20, 20, 21, 13, 12, 12, 10, 7, 3, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 1, 5, 25, 25, 25, 25, 25, 25, 25, 21, 20, 17, 18, 12, 12, 11, 8, 5, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 25, 25, 25, 25, 25, 25, 24, 19, 20, 13, 12, 12, 11, 9, 5, 2, 1, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 19, 25, 25, 25, 25, 25, 25, 23, 25, 25, 24, 15, 11, 9, 6, 2, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 10, 6, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 7, 3, 2, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 22, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 5, 2, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 3, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 21, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 2, 2, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 2, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 13, 25, 25, 24, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25] enc = [39654868, 38564788, 37998449, 36705100, 34811134, 29241290, 21154342, 14031189, 9709480, 10192500, 9488434, 8917703, 8436312, 7963105, 7514984, 7654219, 7487295, 8176216, 9031004, 8970914, 9341190, 9144480, 9366669, 9385331, 9139311, 9514114, 9272562, 8593561, 8340901, 6839039, 5285074, 5402594, 5804603, 5414593, 5336346, 5993555, 7350502, 9029370, 10868398, 13859348, 12111786, 11582283, 11430308, 10556747, 10341351, 10607648, 11143139, 11689137, 11730328, 11611945, 14952608, 18555268, 23156514, 27591411, 29403805, 30676639, 32476022, 36955579, 41264880, 44681781, 44601420, 44143855, 43151161, 42898115]
a = [Int('a[%d]' % i) for i in range(64)] solver = Solver() for i in range(64): tmp = 0 for j in range(64): tmp += a[j] * arr2[j * 64 + i] solver.add(tmp == enc[i]) if solver.check() == sat: result = solver.model() print(result) else: print('Ooops!')
a[25] = 34385 a[6] = 47074 a[23] = 32113 a[34] = 37661 a[12] = 38813 a[18] = 27745 a[14] = 32512 a[16] = 29057 a[27] = 32739 a[19] = 32015 a[33] = 38575 a[58] = 58319 a[4] = 47646 a[31] = 32762 a[7] = 46797 a[11] = 40936 a[24] = 33438 a[36] = 46137 a[5] = 44689 a[21] = 34933 a[2] = 50090 a[29] = 34208 a[3] = 49395 a[41] = 53609 a[10] = 43020 a[28] = 34235 a[9] = 42574 a[22] = 32060 a[30] = 32414 a[1] = 49684 a[17] = 26765 a[13] = 33034 a[20] = 34769 a[35] = 40920 a[43] = 52995 a[37] = 48875 a[8] = 45297 a[0] = 50409 a[15] = 32345 a[32] = 34717 a[26] = 34094 a[40] = 51468 a[63] = 60254 a[51] = 55296 a[50] = 54881 a[44] = 52056 a[52] = 54632 a[45] = 51479 a[38] = 45934 a[39] = 47834 a[61] = 58052 a[62] = 58623 a[56] = 55535 a[59] = 58074 a[47] = 52533 a[55] = 56164 a[42] = 50819 a[60] = 57949 a[57] = 59558 a[54] = 54943 a[53] = 53955 a[48] = 55281 a[49] = 55774 a[46] = 52784
solver = Solver() b = [Int('flag[%d]' % i) for i in range(64)] for i in range(64): tmp = 0 for j in range(64): tmp += b[j] * arr1[j * 64 + i] solver.add(tmp == a[i]) if solver.check() == sat: result = solver.model() print(result) else: print('Failed!') flag = [0 for i in range(64)] flag[31] = 48 flag[38] = 49 flag[36] = 48 flag[37] = 48 flag[55] = 49 flag[0] = 104 flag[62] = 49 flag[13] = 48 flag[53] = 48 flag[51] = 48 flag[44] = 48 flag[28] = 48 flag[25] = 48 flag[18] = 49 flag[16] = 48 flag[27] = 48 flag[50] = 48 flag[33] = 49 flag[43] = 49 flag[57] = 48 flag[61] = 49 flag[6] = 49 flag[48] = 49 flag[24] = 49 flag[59] = 49 flag[49] = 48 flag[21] = 48 flag[30] = 48 flag[32] = 48 flag[4] = 101 flag[58] = 48 flag[10] = 49 flag[63] = 125 flag[26] = 48 flag[45] = 48 flag[29] = 48 flag[20] = 48 flag[46] = 48 flag[12] = 49 flag[2] = 97 flag[39] = 48 flag[56] = 49 flag[8] = 48 flag[11] = 49 flag[35] = 48 flag[41] = 48 flag[3] = 109 flag[7] = 48 flag[60] = 49 flag[1] = 103 flag[19] = 49 flag[22] = 48 flag[9] = 48 flag[15] = 48 flag[40] = 49 flag[5] = 123 flag[42] = 49 flag[34] = 49 flag[54] = 48 flag[23] = 48 flag[14] = 48 flag[17] = 48 flag[47] = 48 flag[52] = 49
for i in flag: print(chr(i), end = "")
|