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