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