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