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