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