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