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