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