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