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