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