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