c 1 = x@0
c 2 = x@1
c 3 = x@2
c 4 = x@4
c 5 = x@3
c 6 = y@0
c 7 = y@1
c 8 = y@2
c 9 = y@4
c 10 = y@3
p cnf 219 628
-11 -4 0
-11 -5 0
4 5 11 0
-12 -3 0
-12 11 0
3 -11 12 0
-13 -2 0
-13 12 0
2 -12 13 0
-14 1 0
-14 13 0
-1 -13 14 0
-15 -9 0
-15 -10 0
9 10 15 0
-16 -8 0
-16 15 0
8 -15 16 0
-17 -7 0
-17 16 0
7 -16 17 0
-18 6 0
-18 17 0
-6 -17 18 0
-19 -14 0
-19 -18 0
14 18 19 0
-20 1 0
-20 6 0
-1 -6 20 0
-21 1 0
-21 7 0
-1 -7 21 0
-22 2 0
-22 6 0
-2 -6 22 0
-23 21 0
-23 22 0
-21 -22 23 0
-24 -21 0
-24 -22 0
21 22 24 0
-25 -23 0
-25 -24 0
23 24 25 0
-26 3 0
-26 6 0
-3 -6 26 0
-27 1 0
-27 8 0
-1 -8 27 0
-28 2 0
-28 7 0
-2 -7 28 0
-29 28 0
-29 -23 0
-28 23 29 0
-30 -28 0
-30 23 0
28 -23 30 0
-31 -29 0
-31 -30 0
29 30 31 0
-32 27 0
-32 -31 0
-27 31 32 0
-33 -27 0
-33 31 0
27 -31 33 0
-34 -32 0
-34 -33 0
32 33 34 0
-35 26 0
-35 34 0
-26 -34 35 0
-36 -26 0
-36 -34 0
26 34 36 0
-37 -35 0
-37 -36 0
35 36 37 0
-38 5 0
-38 6 0
-5 -6 38 0
-39 1 0
-39 10 0
-1 -10 39 0
-40 2 0
-40 8 0
-2 -8 40 0
-41 -27 0
-41 -28 0
27 28 41 0
-42 23 0
-42 -41 0
-23 41 42 0
-43 27 0
-43 28 0
-27 -28 43 0
-44 -42 0
-44 -43 0
42 43 44 0
-45 40 0
-45 44 0
-40 -44 45 0
-46 -40 0
-46 -44 0
40 44 46 0
-47 -45 0
-47 -46 0
45 46 47 0
-48 39 0
-48 -47 0
-39 47 48 0
-49 -39 0
-49 47 0
39 -47 49 0
-50 -48 0
-50 -49 0
48 49 50 0
-51 3 0
-51 7 0
-3 -7 51 0
-52 51 0
-52 -35 0
-51 35 52 0
-53 -51 0
-53 35 0
51 -35 53 0
-54 -52 0
-54 -53 0
52 53 54 0
-55 50 0
-55 -54 0
-50 54 55 0
-56 -50 0
-56 54 0
50 -54 56 0
-57 -55 0
-57 -56 0
55 56 57 0
-58 38 0
-58 57 0
-38 -57 58 0
-59 -38 0
-59 -57 0
38 57 59 0
-60 -58 0
-60 -59 0
58 59 60 0
-61 4 0
-61 6 0
-4 -6 61 0
-62 1 0
-62 9 0
-1 -9 62 0
-63 2 0
-63 10 0
-2 -10 63 0
-64 -39 0
-64 -40 0
39 40 64 0
-65 -44 0
-65 -64 0
44 64 65 0
-66 39 0
-66 40 0
-39 -40 66 0
-67 -65 0
-67 -66 0
65 66 67 0
-68 63 0
-68 67 0
-63 -67 68 0
-69 -63 0
-69 -67 0
63 67 69 0
-70 -68 0
-70 -69 0
68 69 70 0
-71 62 0
-71 -70 0
-62 70 71 0
-72 -62 0
-72 70 0
62 -70 72 0
-73 -71 0
-73 -72 0
71 72 73 0
-74 3 0
-74 8 0
-3 -8 74 0
-75 -51 0
-75 -50 0
51 50 75 0
-76 35 0
-76 -75 0
-35 75 76 0
-77 51 0
-77 50 0
-51 -50 77 0
-78 -76 0
-78 -77 0
76 77 78 0
-79 74 0
-79 78 0
-74 -78 79 0
-80 -74 0
-80 -78 0
74 78 80 0
-81 -79 0
-81 -80 0
79 80 81 0
-82 73 0
-82 -81 0
-73 81 82 0
-83 -73 0
-83 81 0
73 -81 83 0
-84 -82 0
-84 -83 0
82 83 84 0
-85 5 0
-85 7 0
-5 -7 85 0
-86 85 0
-86 -58 0
-85 58 86 0
-87 -85 0
-87 58 0
85 -58 87 0
-88 -86 0
-88 -87 0
86 87 88 0
-89 84 0
-89 -88 0
-84 88 89 0
-90 -84 0
-90 88 0
84 -88 90 0
-91 -89 0
-91 -90 0
89 90 91 0
-92 61 0
-92 91 0
-61 -91 92 0
-93 -61 0
-93 -91 0
61 91 93 0
-94 -92 0
-94 -93 0
92 93 94 0
-95 2 0
-95 9 0
-2 -9 95 0
-96 -62 0
-96 -63 0
62 63 96 0
-97 -67 0
-97 -96 0
67 96 97 0
-98 62 0
-98 63 0
-62 -63 98 0
-99 -97 0
-99 -98 0
97 98 99 0
-100 95 0
-100 -99 0
-95 99 100 0
-101 -95 0
-101 99 0
95 -99 101 0
-102 -100 0
-102 -101 0
100 101 102 0
-103 3 0
-103 10 0
-3 -10 103 0
-104 -74 0
-104 -73 0
74 73 104 0
-105 -78 0
-105 -104 0
78 104 105 0
-106 74 0
-106 73 0
-74 -73 106 0
-107 -105 0
-107 -106 0
105 106 107 0
-108 103 0
-108 107 0
-103 -107 108 0
-109 -103 0
-109 -107 0
103 107 109 0
-110 -108 0
-110 -109 0
108 109 110 0
-111 102 0
-111 -110 0
-102 110 111 0
-112 -102 0
-112 110 0
102 -110 112 0
-113 -111 0
-113 -112 0
111 112 113 0
-114 5 0
-114 8 0
-5 -8 114 0
-115 -85 0
-115 -84 0
85 84 115 0
-116 58 0
-116 -115 0
-58 115 116 0
-117 85 0
-117 84 0
-85 -84 117 0
-118 -116 0
-118 -117 0
116 117 118 0
-119 114 0
-119 118 0
-114 -118 119 0
-120 -114 0
-120 -118 0
114 118 120 0
-121 -119 0
-121 -120 0
119 120 121 0
-122 113 0
-122 -121 0
-113 121 122 0
-123 -113 0
-123 121 0
113 -121 123 0
-124 -122 0
-124 -123 0
122 123 124 0
-125 4 0
-125 7 0
-4 -7 125 0
-126 125 0
-126 -92 0
-125 92 126 0
-127 -125 0
-127 92 0
125 -92 127 0
-128 -126 0
-128 -127 0
126 127 128 0
-129 124 0
-129 -128 0
-124 128 129 0
-130 -124 0
-130 128 0
124 -128 130 0
-131 -129 0
-131 -130 0
129 130 131 0
-132 3 0
-132 9 0
-3 -9 132 0
-133 -103 0
-133 -102 0
103 102 133 0
-134 -107 0
-134 -133 0
107 133 134 0
-135 103 0
-135 102 0
-103 -102 135 0
-136 -134 0
-136 -135 0
134 135 136 0
-137 132 0
-137 136 0
-132 -136 137 0
-138 -132 0
-138 -136 0
132 136 138 0
-139 -137 0
-139 -138 0
137 138 139 0
-140 100 0
-140 -139 0
-100 139 140 0
-141 -100 0
-141 139 0
100 -139 141 0
-142 -140 0
-142 -141 0
140 141 142 0
-143 5 0
-143 10 0
-5 -10 143 0
-144 -114 0
-144 -113 0
114 113 144 0
-145 -118 0
-145 -144 0
118 144 145 0
-146 114 0
-146 113 0
-114 -113 146 0
-147 -145 0
-147 -146 0
145 146 147 0
-148 143 0
-148 147 0
-143 -147 148 0
-149 -143 0
-149 -147 0
143 147 149 0
-150 -148 0
-150 -149 0
148 149 150 0
-151 142 0
-151 -150 0
-142 150 151 0
-152 -142 0
-152 150 0
142 -150 152 0
-153 -151 0
-153 -152 0
151 152 153 0
-154 4 0
-154 8 0
-4 -8 154 0
-155 -125 0
-155 -124 0
125 124 155 0
-156 92 0
-156 -155 0
-92 155 156 0
-157 125 0
-157 124 0
-125 -124 157 0
-158 -156 0
-158 -157 0
156 157 158 0
-159 154 0
-159 158 0
-154 -158 159 0
-160 -154 0
-160 -158 0
154 158 160 0
-161 -159 0
-161 -160 0
159 160 161 0
-162 153 0
-162 -161 0
-153 161 162 0
-163 -153 0
-163 161 0
153 -161 163 0
-164 -162 0
-164 -163 0
162 163 164 0
-165 -132 0
-165 -100 0
132 100 165 0
-166 -136 0
-166 -165 0
136 165 166 0
-167 132 0
-167 100 0
-132 -100 167 0
-168 -166 0
-168 -167 0
166 167 168 0
-169 5 0
-169 9 0
-5 -9 169 0
-170 -143 0
-170 -142 0
143 142 170 0
-171 -147 0
-171 -170 0
147 170 171 0
-172 143 0
-172 142 0
-143 -142 172 0
-173 -171 0
-173 -172 0
171 172 173 0
-174 169 0
-174 173 0
-169 -173 174 0
-175 -169 0
-175 -173 0
169 173 175 0
-176 -174 0
-176 -175 0
174 175 176 0
-177 -168 0
-177 -176 0
168 176 177 0
-178 168 0
-178 176 0
-168 -176 178 0
-179 -177 0
-179 -178 0
177 178 179 0
-180 4 0
-180 10 0
-4 -10 180 0
-181 -154 0
-181 -153 0
154 153 181 0
-182 -158 0
-182 -181 0
158 181 182 0
-183 154 0
-183 153 0
-154 -153 183 0
-184 -182 0
-184 -183 0
182 183 184 0
-185 180 0
-185 184 0
-180 -184 185 0
-186 -180 0
-186 -184 0
180 184 186 0
-187 -185 0
-187 -186 0
185 186 187 0
-188 179 0
-188 -187 0
-179 187 188 0
-189 -179 0
-189 187 0
179 -187 189 0
-190 -188 0
-190 -189 0
188 189 190 0
-191 -180 0
-191 -179 0
180 179 191 0
-192 -184 0
-192 -191 0
184 191 192 0
-193 180 0
-193 179 0
-180 -179 193 0
-194 -192 0
-194 -193 0
192 193 194 0
-195 4 0
-195 9 0
-4 -9 195 0
-196 -169 0
-196 168 0
169 -168 196 0
-197 -173 0
-197 -196 0
173 196 197 0
-198 169 0
-198 -168 0
-169 168 198 0
-199 -197 0
-199 -198 0
197 198 199 0
-200 -195 0
-200 199 0
195 -199 200 0
-201 -194 0
-201 -200 0
194 200 201 0
-202 195 0
-202 -199 0
-195 199 202 0
-203 -201 0
-203 -202 0
201 202 203 0
-204 195 0
-204 194 0
-195 -194 204 0
-205 -195 0
-205 -194 0
195 194 205 0
-206 -204 0
-206 -205 0
204 205 206 0
-207 -199 0
-207 -206 0
199 206 207 0
-208 199 0
-208 206 0
-199 -206 208 0
-209 -207 0
-209 -208 0
207 208 209 0
-210 203 0
-210 -209 0
-203 209 210 0
-211 -190 0
-211 210 0
190 -210 211 0
-212 -164 0
-212 211 0
164 -211 212 0
-213 131 0
-213 212 0
-131 -212 213 0
-214 94 0
-214 213 0
-94 -213 214 0
-215 -60 0
-215 214 0
60 -214 215 0
-216 -37 0
-216 215 0
37 -215 216 0
-217 -25 0
-217 216 0
25 -216 217 0
-218 20 0
-218 217 0
-20 -217 218 0
-219 19 0
-219 218 0
-19 -218 219 0
219 0