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