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