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