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