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