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