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