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