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