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