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