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