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