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