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