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