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