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