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