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