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