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