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