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