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