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