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