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