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