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