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