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