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