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