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