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