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