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