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