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