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