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