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