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