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