c generated by FuzzSAT
p cnf 281 926
2 -3 -4 0
-2 3 -4 0
2 3 4 0
-2 -3 4 0
5 -1 0
5 4 0
1 -4 -5 0
9 7 0
9 -8 0
-7 8 -9 0
10 -6 0
10 -9 0
6 9 -10 0
5 -10 -11 0
-5 10 -11 0
5 10 11 0
-5 -10 11 0
13 10 0
13 -12 0
-10 12 -13 0
15 -16 -17 0
-15 16 -17 0
15 16 17 0
-15 -16 17 0
-14 -17 -18 0
14 17 -18 0
-14 17 18 0
14 -17 18 0
-18 -1 -19 0
18 1 -19 0
-18 1 19 0
18 -1 19 0
21 19 0
21 -20 0
-19 20 -21 0
24 -22 0
24 23 0
22 -23 -24 0
25 21 0
25 24 0
-21 -24 -25 0
26 -3 -27 0
-26 3 -27 0
26 3 27 0
-26 -3 27 0
28 25 0
28 -27 0
-25 27 -28 0
29 3 0
29 -27 0
-3 27 -29 0
-30 12 0
-30 -15 0
-12 15 30 0
-32 -30 0
-32 -31 0
30 31 32 0
-29 -32 -33 0
29 32 -33 0
-29 32 33 0
29 -32 33 0
35 34 0
35 9 0
-34 -9 -35 0
-23 -1 -36 0
23 1 -36 0
-23 1 36 0
23 -1 36 0
-35 -36 -37 0
35 36 -37 0
-35 36 37 0
35 -36 37 0
38 -33 0
38 -37 0
33 37 -38 0
39 -28 0
39 38 0
28 -38 -39 0
40 41 -42 0
-40 -41 -42 0
40 -41 42 0
-40 41 42 0
42 24 -43 0
-42 -24 -43 0
42 -24 43 0
-42 24 43 0
-39 -43 -44 0
39 43 -44 0
-39 43 44 0
39 -43 44 0
-13 -44 -45 0
13 44 -45 0
-13 44 45 0
13 -44 45 0
46 -6 -47 0
-46 6 -47 0
46 6 47 0
-46 -6 47 0
48 34 0
48 47 0
-34 -47 -48 0
-50 41 0
-50 -2 0
-41 2 50 0
26 -50 -51 0
-26 50 -51 0
26 50 51 0
-26 -50 51 0
-52 15 0
-52 7 0
-15 -7 52 0
-53 -51 0
-53 52 0
51 -52 53 0
49 -53 -54 0
-49 53 -54 0
49 53 54 0
-49 -53 54 0
55 -50 0
55 -20 0
50 20 -55 0
-56 -14 0
-56 55 0
14 -55 56 0
54 56 -57 0
-54 -56 -57 0
54 -56 57 0
-54 56 57 0
58 48 0
58 57 0
-48 -57 -58 0
59 45 0
59 58 0
-45 -58 -59 0
11 59 -60 0
-11 -59 -60 0
11 -59 60 0
-11 59 60 0
61 25 0
61 53 0
-25 -53 -61 0
-63 -35 0
-63 3 0
35 -3 63 0
-62 63 -64 0
62 -63 -64 0
-62 -63 64 0
62 63 64 0
64 -52 -65 0
-64 52 -65 0
64 52 65 0
-64 -52 65 0
67 -66 0
67 -7 0
66 7 -67 0
68 26 0
68 -23 0
-26 23 -68 0
70 68 0
70 -69 0
-68 69 -70 0
-71 70 0
-71 19 0
-70 -19 71 0
-46 62 -72 0
46 -62 -72 0
-46 -62 72 0
46 62 72 0
72 -12 -73 0
-72 12 -73 0
72 12 73 0
-72 -12 73 0
74 -71 0
74 -73 0
71 73 -74 0
67 -74 -75 0
-67 74 -75 0
67 74 75 0
-67 -74 75 0
76 66 0
76 -69 0
-66 69 -76 0
78 41 0
78 -77 0
-41 77 -78 0
79 76 0
79 78 0
-76 -78 -79 0
-80 75 0
-80 -79 0
-75 79 80 0
-65 80 -81 0
65 -80 -81 0
-65 -80 81 0
65 80 81 0
82 -73 0
82 -41 0
73 41 -82 0
83 -81 0
83 82 0
81 -82 -83 0
61 83 -84 0
-61 -83 -84 0
61 -83 84 0
-61 83 84 0
-60 84 -85 0
60 -84 -85 0
-60 -84 85 0
60 84 85 0
86 46 0
86 3 0
-46 -3 -86 0
-87 -26 0
-87 -86 0
26 86 87 0
77 -87 -88 0
-77 87 -88 0
77 87 88 0
-77 -87 88 0
-90 20 0
-90 -89 0
-20 89 90 0
1 -90 -91 0
-1 90 -91 0
1 90 91 0
-1 -90 91 0
-91 34 -92 0
91 -34 -92 0
-91 -34 92 0
91 34 92 0
93 -88 0
93 92 0
88 -92 -93 0
-4 93 -94 0
4 -93 -94 0
-4 -93 94 0
4 93 94 0
95 -49 0
95 -62 0
49 62 -95 0
-97 -49 0
-97 -96 0
49 96 97 0
98 -95 0
98 97 0
95 -97 -98 0
94 98 -99 0
-94 -98 -99 0
94 -98 99 0
-94 98 99 0
-100 -2 0
-100 9 0
2 -9 100 0
-101 17 0
-101 -15 0
-17 15 101 0
102 -101 0
102 26 0
101 -26 -102 0
-100 102 -103 0
100 -102 -103 0
-100 -102 103 0
100 102 103 0
104 16 0
104 1 0
-16 -1 -104 0
15 -14 -105 0
-15 14 -105 0
15 14 105 0
-15 -14 105 0
-104 105 -106 0
104 -105 -106 0
-104 -105 106 0
104 105 106 0
-107 -106 0
-107 20 0
106 -20 107 0
108 -103 0
108 -107 0
103 107 -108 0
-99 108 -109 0
99 -108 -109 0
-99 -108 109 0
99 108 109 0
-8 -46 -110 0
8 46 -110 0
-8 46 110 0
8 -46 110 0
111 31 0
111 -110 0
-31 110 -111 0
-112 52 0
-112 -111 0
-52 111 112 0
-112 71 -113 0
112 -71 -113 0
-112 -71 113 0
112 71 113 0
114 106 0
114 -34 0
-106 34 -114 0
114 -105 -115 0
-114 105 -115 0
114 105 115 0
-114 -105 115 0
-116 113 0
-116 115 0
-113 -115 116 0
-117 69 0
-117 -20 0
-69 20 117 0
-118 -117 0
-118 104 0
117 -104 118 0
116 118 -119 0
-116 -118 -119 0
116 -118 119 0
-116 118 119 0
120 89 0
120 -24 0
-89 24 -120 0
-69 -102 -121 0
69 102 -121 0
-69 102 121 0
69 -102 121 0
-122 120 0
-122 -121 0
-120 121 122 0
123 -55 0
123 10 0
55 -10 -123 0
-124 -122 0
-124 123 0
122 -123 124 0
-125 -119 0
-125 124 0
119 -124 125 0
-26 63 -126 0
26 -63 -126 0
-26 -63 126 0
26 63 126 0
126 19 -127 0
-126 -19 -127 0
126 -19 127 0
-126 19 127 0
127 4 -128 0
-127 -4 -128 0
127 -4 128 0
-127 4 128 0
-29 129 -130 0
29 -129 -130 0
-29 -129 130 0
29 129 130 0
131 -128 0
131 -130 0
128 130 -131 0
131 -20 -132 0
-131 20 -132 0
131 20 132 0
-131 -20 132 0
-133 125 0
-133 132 0
-125 -132 133 0
134 -15 0
134 -62 0
15 62 -134 0
-62 -134 -135 0
62 134 -135 0
-62 134 135 0
62 -134 135 0
42 112 -136 0
-42 -112 -136 0
42 -112 136 0
-42 112 136 0
137 135 0
137 136 0
-135 -136 -137 0
-138 133 0
-138 137 0
-133 -137 138 0
-139 -109 0
-139 -138 0
109 138 139 0
-140 -85 0
-140 139 0
85 -139 140 0
-42 -35 -141 0
42 35 -141 0
-42 35 141 0
42 -35 141 0
-63 -129 -142 0
63 129 -142 0
-63 129 142 0
63 -129 142 0
-143 142 0
-143 -20 0
-142 20 143 0
144 68 0
144 6 0
-68 -6 -144 0
-143 144 -145 0
143 -144 -145 0
-143 -144 145 0
143 144 145 0
146 141 0
146 -145 0
-141 145 -146 0
-147 -9 0
-147 -96 0
9 96 147 0
-148 147 0
-148 -40 0
-147 40 148 0
-149 -34 0
-149 -50 0
34 50 149 0
-150 -22 0
-150 -34 0
22 34 150 0
-151 -46 0
-151 50 0
46 -50 151 0
-152 150 0
-152 151 0
-150 -151 152 0
153 149 0
153 -152 0
-149 152 -153 0
-148 153 -154 0
148 -153 -154 0
-148 -153 154 0
148 153 154 0
155 -18 0
155 37 0
18 -37 -155 0
27 96 -156 0
-27 -96 -156 0
27 -96 156 0
-27 96 156 0
-157 156 0
-157 63 0
-156 -63 157 0
158 -155 0
158 157 0
155 -157 -158 0
-154 158 -159 0
154 -158 -159 0
-154 -158 159 0
154 158 159 0
130 -160 0
-130 -160 0
-161 160 0
-161 -8 0
-160 8 161 0
-162 4 0
-162 129 0
-4 -129 162 0
-163 162 0
-163 -93 0
-162 93 163 0
-163 104 -164 0
163 -104 -164 0
-163 -104 164 0
163 104 164 0
-161 -164 -165 0
161 164 -165 0
-161 164 165 0
161 -164 165 0
-166 -36 0
-166 53 0
36 -53 166 0
167 -166 0
167 -104 0
166 104 -167 0
168 69 0
168 36 0
-69 -36 -168 0
169 167 0
169 -168 0
-167 168 -169 0
170 -165 0
170 -169 0
165 169 -170 0
-159 -170 -171 0
159 170 -171 0
-159 170 171 0
159 -170 171 0
-172 146 0
-172 171 0
-146 -171 172 0
-26 1 -173 0
26 -1 -173 0
-26 -1 173 0
26 1 173 0
-63 -26 -174 0
63 26 -174 0
-63 26 174 0
63 -26 174 0
-175 -173 0
-175 174 0
173 -174 175 0
-176 -113 0
-176 -34 0
113 34 176 0
-177 175 0
-177 -176 0
-175 176 177 0
178 -106 0
178 77 0
106 -77 -178 0
179 -88 0
179 178 0
88 -178 -179 0
-180 88 0
-180 -179 0
-88 179 180 0
-181 -180 0
-181 53 0
180 -53 181 0
-96 37 -182 0
96 -37 -182 0
-96 -37 182 0
96 37 182 0
2 182 -183 0
-2 -182 -183 0
2 -182 183 0
-2 182 183 0
-183 87 -184 0
183 -87 -184 0
-183 -87 184 0
183 87 184 0
-185 184 0
-185 41 0
-184 -41 185 0
181 185 -186 0
-181 -185 -186 0
181 -185 186 0
-181 185 186 0
188 -52 0
188 -187 0
52 187 -188 0
-189 -64 0
-189 -188 0
64 188 189 0
-190 186 0
-190 -189 0
-186 189 190 0
-92 168 -191 0
92 -168 -191 0
-92 -168 191 0
92 168 191 0
-192 -89 0
-192 62 0
89 -62 192 0
193 -191 0
193 -192 0
191 192 -193 0
-190 -193 -194 0
190 193 -194 0
-190 193 194 0
190 -193 194 0
-177 194 -195 0
177 -194 -195 0
-177 -194 195 0
177 194 195 0
-196 -172 0
-196 195 0
172 -195 196 0
-197 52 0
-197 168 0
-52 -168 197 0
198 -105 0
198 -46 0
105 46 -198 0
-199 -77 0
-199 76 0
77 -76 199 0
-200 -198 0
-200 -199 0
198 199 200 0
-201 27 0
-201 -62 0
-27 62 201 0
-202 201 0
-202 -68 0
-201 68 202 0
-3 8 -203 0
3 -8 -203 0
-3 -8 203 0
3 8 203 0
-203 91 -204 0
203 -91 -204 0
-203 -91 204 0
203 91 204 0
205 -204 0
205 110 0
204 -110 -205 0
202 205 -206 0
-202 -205 -206 0
202 -205 206 0
-202 205 206 0
2 46 -207 0
-2 -46 -207 0
2 -46 207 0
-2 46 207 0
208 -180 0
208 207 0
180 -207 -208 0
-209 -206 0
-209 208 0
206 -208 209 0
-210 66 0
-210 -127 0
-66 127 210 0
-18 88 -211 0
18 -88 -211 0
-18 -88 211 0
18 88 211 0
-212 211 0
-212 -55 0
-211 55 212 0
210 -212 -213 0
-210 212 -213 0
210 212 213 0
-210 -212 213 0
-214 -209 0
-214 -213 0
209 213 214 0
-215 -200 0
-215 214 0
200 -214 215 0
-197 -215 -216 0
197 215 -216 0
-197 215 216 0
197 -215 216 0
-217 -64 0
-217 -162 0
64 162 217 0
-218 217 0
-218 -10 0
-217 10 218 0
96 -179 -219 0
-96 179 -219 0
96 179 219 0
-96 -179 219 0
220 16 0
220 -15 0
-16 15 -220 0
-221 -178 0
-221 -4 0
178 4 221 0
222 -220 0
222 -221 0
220 221 -222 0
-223 -219 0
-223 222 0
219 -222 223 0
224 218 0
224 223 0
-218 -223 -224 0
225 -183 0
225 -22 0
183 22 -225 0
147 -225 -226 0
-147 225 -226 0
147 225 226 0
-147 -225 226 0
-227 226 0
-227 130 0
-226 -130 227 0
-187 180 -228 0
187 -180 -228 0
-187 -180 228 0
187 180 228 0
112 63 -229 0
-112 -63 -229 0
112 -63 229 0
-112 63 229 0
-228 229 -230 0
228 -229 -230 0
-228 -229 230 0
228 229 230 0
-231 227 0
-231 230 0
-227 -230 231 0
-232 224 0
-232 231 0
-224 -231 232 0
-233 216 0
-233 232 0
-216 -232 233 0
234 -142 0
234 -27 0
142 27 -234 0
235 -33 0
235 25 0
33 -25 -235 0
-234 -235 -236 0
234 235 -236 0
-234 235 236 0
234 -235 236 0
236 -62 -237 0
-236 62 -237 0
236 62 237 0
-236 -62 237 0
238 -147 0
238 -78 0
147 78 -238 0
239 -237 0
239 -238 0
237 238 -239 0
241 -33 0
241 240 0
33 -240 -241 0
242 22 0
242 126 0
-22 -126 -242 0
-243 241 0
-243 242 0
-241 -242 243 0
-244 29 0
-244 42 0
-29 -42 244 0
-245 -90 0
-245 244 0
90 -244 245 0
-246 -22 0
-246 -86 0
22 86 246 0
247 246 0
247 -23 0
-246 23 -247 0
-248 -245 0
-248 247 0
245 -247 248 0
-249 -188 0
-249 106 0
188 -106 249 0
182 183 -250 0
-182 -183 -250 0
182 -183 250 0
-182 183 250 0
251 -86 0
251 178 0
86 -178 -251 0
250 -251 -252 0
-250 251 -252 0
250 251 252 0
-250 -251 252 0
-249 -252 -253 0
249 252 -253 0
-249 252 253 0
249 -252 253 0
254 -51 0
254 55 0
51 -55 -254 0
255 254 0
255 -102 0
-254 102 -255 0
256 -253 0
256 255 0
253 -255 -256 0
257 -248 0
257 -256 0
248 256 -257 0
-258 2 0
-258 4 0
-2 -4 258 0
-259 -258 0
-259 -6 0
258 6 259 0
261 -73 0
261 260 0
73 -260 -261 0
-262 259 0
-262 -261 0
-259 261 262 0
-263 -2 0
-263 142 0
2 -142 263 0
263 191 -264 0
-263 -191 -264 0
263 -191 264 0
-263 191 264 0
265 31 0
265 -263 0
-31 263 -265 0
113 -265 -266 0
-113 265 -266 0
113 265 266 0
-113 -265 266 0
263 -266 -267 0
-263 266 -267 0
263 266 267 0
-263 -266 267 0
264 267 -268 0
-264 -267 -268 0
264 -267 268 0
-264 267 268 0
-269 20 0
-269 -26 0
-20 26 269 0
-102 269 -270 0
102 -269 -270 0
-102 -269 270 0
102 269 270 0
-271 -30 0
-271 -270 0
30 270 271 0
272 -89 0
272 160 0
89 -160 -272 0
-273 271 0
-273 -272 0
-271 272 273 0
274 -268 0
274 -273 0
268 273 -274 0
275 -262 0
275 274 0
262 -274 -275 0
-257 275 -276 0
257 -275 -276 0
-257 -275 276 0
257 275 276 0
277 -243 0
277 -276 0
243 276 -277 0
278 -239 0
278 277 0
239 -277 -278 0
279 233 0
279 278 0
-233 -278 -279 0
280 -196 0
280 279 0
196 -279 -280 0
-140 -280 -281 0
140 280 -281 0
-140 280 281 0
140 -280 281 0
184 177 -155 192 0
34 -53 280 0
234 114 0
248 -114 82 140 0
16 221 -52 -253 0
-122 83 0
171 51 -229 189 0
186 -5 -104 0
-243 -50 252 0
-39 -236 -80 0
-257 42 -96 0
109 -77 141 0
-250 117 -131 -207 57 0
-12 160 -113 -137 -76 234 0
98 -217 -110 -254 58 281 0
64 -243 18 -90 161 0
215 85 -45 0
65 261 -53 0
-166 -183 0
-168 90 -277 151 121 -144 0
-51 170 -185 -252 -180 0
-149 184 27 -228 0
-70 264 226 -169 0
179 -3 0
-254 59 -156 255 0
69 -86 270 -42 0
-91 140 0
-3 184 -85 192 0
155 46 -11 -115 0
153 -147 0
-195 -281 -127 -191 197 141 0
180 32 251 -21 0
111 85 149 -105 0
-2 -224 -14 159 84 0
-53 -192 0
-162 128 -188 -27 136 0
-128 -104 -87 2 -109 0
46 181 188 249 105 0
-97 269 -103 0
-243 197 0
232 244 -28 265 102 0
-79 195 -117 190 0
276 -6 -100 -237 98 29 0
65 3 0
249 140 63 -181 4 197 0
-64 -55 -244 0
99 -165 -100 142 -84 0
-92 112 278 -71 0
197 -111 26 -216 215 -110 0
-54 273 243 0
104 -260 -269 0
232 -111 -21 0
26 -181 51 -56 -3 0
-221 241 142 -184 0
-9 241 256 -243 0
42 -246 -164 0
-169 -23 0
64 -21 -107 -9 112 245 0
109 -191 -33 0
94 -66 137 119 0
184 -153 -167 -118 214 0
-47 -144 25 218 0
-160 191 247 0
-13 165 -79 -248 -86 0
-92 244 0
102 -142 -122 0
123 -138 0
244 -110 -171 178 -21 0
-140 53 0
-168 -254 0
166 -56 181 280 177 0
103 152 0
243 92 214 158 164 122 0
65 -187 208 0
-81 38 176 0
204 -246 -233 90 273 0
-70 -177 -10 0
141 -140 241 -34 0
195 -52 233 30 10 -185 0
-120 13 -248 80 117 -232 0
33 -152 -133 140 0
209 -88 -221 148 -147 197 0
-105 87 0
211 -242 -17 -25 -238 127 0
281 0