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