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