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