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