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