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