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