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