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