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