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