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