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