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