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