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