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