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