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