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