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