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