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