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