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