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