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