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