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