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