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