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