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