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