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