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