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