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