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