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