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