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