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