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