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