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