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