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