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