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