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