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