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