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