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