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