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