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