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