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