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