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