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