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