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