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