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