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