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