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