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