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