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