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