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