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