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