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