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