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