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