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