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