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