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