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