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