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