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