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