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 100 430 15 -99 37 0 67 -89 -56 0 -72 -23 -54 0 31 35 -58 0 -49 22 -24 0 1 -33 -83 0 -45 27 63 0 77 -21 59 0 -24 2 -46 0 -49 68 89 0 57 -18 -39 0 -15 -99 -25 0 -14 75 -93 0 84 28 -67 0 -96 58 -52 0 90 87 88 0 -26 42 40 0 24 33 12 0 81 88 -43 0 -31 -12 8 0 53 84 -25 0 81 -38 92 0 -59 11 43 0 86 -7 34 0 -80 -84 -61 0 25 -18 39 0 -100 -39 -87 0 2 -18 85 0 91 74 -18 0 74 -81 54 0 89 94 -37 0 -77 42 -33 0 38 -34 -9 0 -34 -68 -69 0 -21 -66 52 0 93 88 -13 0 -24 -92 97 0 -47 93 63 0 51 -49 -8 0 90 -20 -65 0 -61 87 -52 0 29 -40 58 0 53 -42 6 0 -56 -47 -70 0 64 -56 -89 0 92 58 -69 0 -10 -60 25 0 -80 -37 -62 0 -6 -8 75 0 -34 27 33 0 -54 81 -84 0 -6 -72 94 0 52 92 75 0 41 51 39 0 -59 54 -37 0 -7 -69 -41 0 -59 71 -25 0 65 94 71 0 73 -71 -65 0 -21 46 -39 0 -18 43 -22 0 11 91 -57 0 -14 8 93 0 -99 20 -94 0 -48 52 -25 0 -41 -26 4 0 49 95 -27 0 -4 44 77 0 19 -27 -43 0 92 38 24 0 -77 65 59 0 16 -75 -37 0 -12 -84 10 0 -11 99 -64 0 26 3 91 0 82 -96 80 0 83 92 -82 0 -85 46 45 0 -31 -44 23 0 48 -22 -37 0 54 -52 50 0 39 -75 17 0 81 -79 96 0 -50 -3 -72 0 6 -46 -90 0 97 -37 12 0 -71 9 -79 0 38 10 50 0 61 -84 25 0 -1 62 -67 0 -50 1 -88 0 66 -18 44 0 -42 4 -64 0 -35 -22 9 0 -68 38 98 0 -8 -42 -35 0 -34 6 -58 0 -92 52 -55 0 40 60 -14 0 -79 -95 -28 0 -24 60 -12 0 50 62 5 0 59 -30 -65 0 7 -24 -50 0 10 51 70 0 8 51 81 0 18 -59 71 0 36 25 39 0 91 -45 46 0 -16 74 -69 0 -7 19 -46 0 -97 -55 -14 0 76 13 4 0 -37 4 86 0 -100 59 24 0 63 51 -54 0 -62 36 45 0 -54 -79 34 0 -100 29 -51 0 -35 -10 -54 0 93 39 -49 0 -37 -8 23 0 -4 -37 -94 0 25 35 78 0 45 -82 -71 0 61 27 10 0 -15 -36 29 0 33 -65 -69 0 -20 86 87 0 -10 -66 -97 0 -44 -48 2 0 1 -69 52 0 61 98 77 0 -82 44 23 0 -84 50 -10 0 -56 73 -44 0 73 -27 67 0 37 16 -30 0 -51 -27 97 0 17 -80 86 0 -22 -15 87 0 64 -45 -40 0 -62 6 -10 0 44 70 -83 0 -77 -59 57 0 -76 -7 31 0 76 -37 48 0 9 29 23 0 -74 63 -10 0 -34 79 -11 0 6 -17 -2 0 -40 -55 -10 0 -5 78 -27 0 70 -87 77 0 59 68 39 0 -55 25 36 0 31 59 -19 0 23 5 1 0 -16 -71 -10 0 -21 55 -67 0 94 57 100 0 -38 -79 -63 0 -52 -19 -95 0 -76 -84 -66 0 -85 -96 16 0 26 -48 75 0 -30 -13 -1 0 -82 -21 -17 0 72 49 68 0 99 -18 -38 0 33 94 40 0 30 49 -29 0 28 -22 -18 0 -29 69 -39 0 -38 4 -90 0 68 -50 -52 0 -23 86 -20 0 -48 -44 -81 0 -56 16 -46 0 -66 49 -55 0 -14 -92 -22 0 -37 -21 -64 0 -16 -19 23 0 74 40 26 0 71 -100 86 0 98 68 -1 0 -98 69 -19 0 -41 40 -8 0 -74 10 -31 0 37 100 63 0 31 23 86 0 29 40 87 0 36 42 -52 0 -34 -80 97 0 -28 16 -26 0 -8 -67 73 0 -12 -26 -54 0 -10 -9 96 0 48 86 -81 0 -70 -78 75 0 46 -76 -78 0 -33 -81 -100 0 41 88 80 0 38 97 -17 0 -78 11 43 0 64 -52 -86 0 15 -3 35 0 -86 -30 1 0 97 5 -45 0 78 -1 96 0 31 -17 53 0 71 -72 25 0 19 72 44 0 68 34 15 0 -99 25 -39 0 96 -76 -9 0 -71 -63 37 0 -10 87 95 0 -63 -73 66 0 -16 -84 -37 0 -46 73 58 0 -19 -92 -12 0 -78 96 -67 0 -4 -12 45 0 82 -4 -15 0 -1 -3 -65 0 7 74 -76 0 -99 -6 58 0 -37 81 18 0 13 32 -11 0 -18 51 71 0 67 16 100 0 -5 -33 34 0 -69 35 92 0 93 -29 74 0 71 -73 -74 0 -67 -22 97 0 95 69 -63 0 40 -100 96 0 73 -79 -41 0 69 -52 68 0 24 59 44 0 51 19 76 0 -74 87 -7 0 82 91 -72 0 -18 6 -5 0 -8 -72 -56 0 59 -42 98 0 41 -29 31 0 41 80 -39 0 -67 19 81 0 69 -11 -100 0 3 -20 -33 0 -45 95 17 0 -24 -84 -94 0 37 63 13 0 45 2 -27 0 -35 28 -8 0 -54 73 -57 0 -84 72 -83 0 -72 -71 -42 0 100 -32 76 0 14 -10 -28 0 84 -30 -28 0 40 -83 -48 0 1 32 52 0 -16 15 71 0 93 -55 56 0 75 -60 -62 0 78 -39 43 0 -6 61 34 0 -96 18 64 0 -13 2 59 0 -100 -97 -95 0 -22 76 -34 0 -66 -7 -55 0 49 59 -75 0 -16 38 86 0 11 -6 3 0 100 -88 -77 0 -26 17 84 0 36 -65 6 0 -94 -92 -67 0 -87 -77 78 0 -91 81 -31 0 45 39 99 0 -74 -55 -80 0 -9 58 48 0 48 23 -91 0 70 -2 -54 0 -82 13 6 0 -96 -14 78 0 -31 -1 99 0 -92 25 -59 0 55 19 72 0 -74 -1 -54 0 -3 -78 -7 0 22 -83 -1 0 56 51 -2 0 -85 -87 -70 0 97 68 -89 0 43 50 -48 0 49 -51 82 0 26 27 92 0 78 -25 11 0 36 78 73 0 95 70 -69 0 42 69 48 0 -65 -44 -45 0 -81 -49 -11 0 -96 -32 -69 0 -88 -51 -65 0 54 -36 -52 0 -20 -24 -13 0 -50 -60 31 0 52 46 58 0 -15 -2 -65 0 63 10 -94 0 -83 -31 -75 0 78 45 -14 0 -35 -56 10 0 -6 -90 -25 0 29 31 92 0 73 27 33 0 2 99 -72 0 -79 41 33 0 12 39 -98 0 17 -37 96 0 11 -32 -66 0 70 -81 -87 0 -19 -74 -35 0 -59 73 6 0 21 26 51 0 55 -44 40 0 -9 -56 -99 0 89 -16 67 0 -90 -25 1 0 -9 1 -34 0 68 -71 -11 0 26 -100 52 0 -18 83 64 0 12 -95 54 0 -21 -98 -35 0 22 24 32 0 -57 12 80 0 -99 -90 92 0 94 -89 76 0 -26 75 -44 0 2 -55 16 0 61 43 40 0 -68 22 35 0 -81 97 -18 0 65 28 70 0 2 9 55 0 -45 2 83 0 -31 -9 28 0 94 49 28 0 -7 -68 -58 0 76 -78 75 0 -71 40 -18 0 -60 54 69 0 18 13 -85 0 75 31 56 0 -98 82 9 0 88 84 -43 0 65 -97 20 0 -69 1 -50 0 -41 -20 4 0 28 49 91 0 -40 8 87 0 -49 78 20 0 -5 80 3 0 29 -74 67 0 41 98 -67 0 36 -74 94 0 -46 -5 -85 0 -68 78 74 0 -19 -60 80 0 -4 -33 -48 0 56 100 -50 0 67 -17 41 0 -100 -67 10 0 -89 58 96 0 77 82 -94 0 -2 -45 31 0 8 -32 59 0 -84 63 14 0 8 -22 70 0 49 72 1 0 17 -20 -91 0 89 78 -88 0 95 9 14 0 -20 9 -68 0 7 61 -35 0 53 -20 71 0 -98 55 19 0 36 97 -52 0 -95 24 -61 0 -25 19 34 0 -10 78 56 0 22 19 -76 0 84 -39 -74 0 88 82 1 0 -21 68 -31 0 91 37 -34 0 67 -39 -72 0 -19 -63 14 0 -69 86 83 0 81 55 95 0 -67 100 -57 0 54 -11 -13 0 1 -71 -54 0 -16 -31 -37 0 25 -80 26 0 -40 -58 -34 0 -71 11 88 0 75 -37 -10 0 80 -66 2 0 87 88 -81 0 -46 47 -29 0 57 -13 96 0 -83 -71 68 0 -63 -79 84 0 65 -82 35 0 16 40 88 0 29 75 44 0 56 -1 10 0 41 56 -86 0 71 84 -63 0 46 -44 95 0 % 0