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