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