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