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