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