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