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