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