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