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