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