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