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