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