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