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