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