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