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