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