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