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