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