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