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