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