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