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