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