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