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