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