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