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