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