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