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