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