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