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