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