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